[Gcl-devel] Re: (si::sgc-on nil)

[Camm Maguire]

Greetings!  I'm happy to announce a fix just committed into CVS HEAD
and version 2.6.1.  Many thanks for the report, which made it
possible. 

For those interested, GCL's gbc touches structure headers when the
body is written and sgc is enabled, to make sure the page containing
the header is made writable and therefore passes through the mark
phase of the sgbc.  SGC is a C define which is typically selected or
not in h/config.h.  There is a mechanism in the makefile to grab
certain defines from config.h for use in cmpinclude.h (the compiler
header file) if they are between comments /* Begin for cmpinclude */
and /* End for cmpinclude */ Most of our recently created
machine-specific config.h files do not have these magic comments as we
were unaware of them -- consequently SGC was never defined in
cmpinclude.h, and structure headers were not touched when the body was
written.  As I feel the "comment sandwich" method is quite fragile,
I've added a line in the main makefile to pass config.h through cpp to
determine if SGC is defined, and then append to cmpinclude.h as
necessary.  We do need to robustify header dependencies at some point.

This fixes all the reported difficulties in compiling pc-nqthm-1992.
It does not yet address the issue of a larger stack space being
required to complete the tests in this software as compared with
earlier GCL versions.  I will try to take a look at this at some
point, but I have a hunch.  In response to Paul's compiler stress
testers, we have plugged a few holes in GCL's compiler in which the
side effects of certain local function calls were not properly
calculated for the purposes of ensuring correct ordering.  To address
this, we have added an 'info' slot into the compiler's 'fun'
structure, and used this to pass a list of changed variables up
through the calling list structure and ensure proper ordering through
GCL's pre-existing mechanism in the function args-info-changed-vars.
While this works, I do know that this can result in quite a bit more
consing.  The original info merging code used 'append' to join
sublists of changed variables, but with our addition, one file in
maxima (nusum.lisp) took an extraordinary amount of time to compile,
so we altered the simple append call to an addition of only unique
elements.  My guess is that the newly enlarged stack requirements are
correct and stem from this issue.  The more local calls (flet and
labels) one has, the more the added overhead.  Perhaps someone might
suggest a more efficient algorithm if there is one at some point.

Many thanks for this error report, which had revealed an issue
invisible in acl2, axiom, maxima, and the ansi-test suite.  I'd like
to add these nqthm regression tests to our informal list of GCL
testers which must pass for any stable release.  If anyone knows of
other such code suitable for this purpose, I would be interested. 

I will try to look at Paul's latest ordering issue (appearing only
with safety 3), and then push out a new stable.  As you may know, our
temporary distribution site is down awaiting the Debian sysadmin's
verification against the recent compromise attempt.

Take care,

Robert Boyer <address@hidden> writes:

> > How did you run the pc-nqthm steps when sidestepping the
> > save in the nqthm-1992 build?
> 
> I think that I have sent you the following message twice before (not that
> I mind a bit, I am so grateful to you for looking into these things).  The
> answer to your question above, the exact sequence of commands, starts
> below at the ----------
> 
> Bob
> 
> >From boyer Mon Nov 17 13:26:28 -0600 2003
> To: address@hidden
> Cc: kaufmann
> Subject: save probably
> 
> 
> Here is a tiny bit more evidence that the problem may be a bug in
> si::save-system.
> 
> In a previous message I reported that if one skips the save operation, then
> the apparent compiler bug that Matt pointed to does not arise.
> Unfortunately, that message's transcript ended with a value stack overflow,
> indicating another possible uncertainty about the nature of the problem.
> However, the value stack overflow is just a normal sort of thing.  I
> conjecture that somewhere between our build of gcl-2.3.8 and our build of
> gcl-2.6.1 there may have been some change to the size of the value stack or
> to what gets pushed onto the value stack by gcl.  If I augment the previously
> sent commands with a simple
> 
>   (SETQ SI::*MULTIPLY-STACKS* 16)
> 
> then Matt's *very* extensive example collection replays without any problem.
> 
> To summarize: given a high enough size for the stacks, no bug arises in the
> standard compilation and loading of nqthm-1992 and the standard compilation
> and loading of pc-nqthm-1992 and the execution of the huge set of
> pc-nqthm-1992 examples, provided no save is done, whereas a bug arises at the
> pc-nqthm compilation stage if before that compilation is begun a save and
> restart from the save is done.
> 
> Here is what I typed, and then below that is the output, including evidence
> of completion of all the pc-nqthm examples.
> 
> -------------------------------------------------------------------------------
> Again, for this example, the directory
> 
>   /u/boyer/nqthm-2nd/nqthm-1992
> contains the unzipped and untarred version of
>   ftp://ftp.cs.utexas.edu/pub/boyer/nqthm/nqthm-1992.tar.gz
> 
> and the directory
>   /u/boyer/pc-nqthm-1992
> contains the unzipped and untarred version of
>   ftp://ftp.cs.utexas.edu/pub/boyer/pc-nqthm/pc-nqthm-1992.tar.gz
> 
> 
> cd /u/boyer/nqthm-2nd/nqthm-1992
> make clean
> set LISP=gcl-2.6.1
> $LISP
> (defun si::save-system (x) nil)
> (load "make/compile.lisp")
> C-C C-Z temporary exit to shell
> echo '"'${LISP}'" "'`pwd`'"' > nqthm-1992-tmp
> fg
> (load "make/save.lisp")
> C-C C-Z temporary exit to shell
> cd /u/boyer/pc-nqthm-1992
> make clean
> make clean-giant-examples
> set CMULISP=cmulisp
> fg
> (SETQ SI::*MULTIPLY-STACKS* 16)
> (si::chdir "/u/boyer/pc-nqthm-1992")
> (load "make/compile.lisp")
> C-C C-Z temporary exit to shell
> echo '"'${CMULISP}'" "'`pwd`'"' > pc-nqthm-1992-tmp
> fg
> (load "make/save.lisp")
> (si::chdir "examples")
> (load "dir.lisp")
> (load "driver.lisp")
> 
> -------------------------------------------------------------------------------
> Here is the ouput of the above input, an entirely successful execution of
> many, many pc-nqthm-examples.
> 
> % cd /u/boyer/nqthm-2nd/nqthm-1992
> % make clean
> rm -f make/compile-success nqthm-1992 TAGS
> rm -f *.o *.c *.h *.data *.sbin *.lbin *.fasl *.sparcf \
>  make/tiny-test.* *saved_nqthm-1992 make/tmp.* *.log
> % set LISP=gcl-2.6.1
> % $LISP
> GCL (GNU Common Lisp)  (2.6.1) Sun Nov 16 04:38:18 CST 2003
> Licensed under GNU Library General Public License
> Dedicated to the memory of W. Schelter
> 
> Use (help) to get some basic information on how to use GCL.
> Loading init.lsp
> Finished loading init.lsp
> 
> >(defun si::save-system (x) nil)
> 
> SYSTEM:SAVE-SYSTEM
> 
> >(load "make/compile.lisp")
> 
> Loading make/compile.lisp
> Loading nqthm.lisp
> Finished loading nqthm.lisp
> Loading sloop.o
> start address -T 0x873d000 Finished loading sloop.o
> Loading basis.o
> start address -T 0x874b000 Finished loading basis.o
> Loading genfact.o
> start address -T 0x875ef60 Finished loading genfact.o
> Loading events.o
> start address -T 0x87a5000 Finished loading events.o
> Loading sloop.o
> start address -T 0x8966000 Finished loading sloop.o
> Loading basis.o
> start address -T 0x87ac000 Finished loading basis.o
> Loading genfact.o
> start address -T 0x873c060 Finished loading genfact.o
> Loading events.o
> start address -T 0x8975ea0 Finished loading events.o
> Loading code-1-a.o
> start address -T 0x8989000 Finished loading code-1-a.o
> Loading code-b-d.o
> start address -T 0x89bc000 Finished loading code-b-d.o
> Loading code-e-m.o
> start address -T 0x89d1000 Finished loading code-e-m.o
> Loading code-n-r.o
> start address -T 0x8a11000 Finished loading code-n-r.o
> Loading code-s-z.o
> start address -T 0x89e5660 Finished loading code-s-z.o
> Loading io.o
> start address -T 0x87b4300 Finished loading io.o
> Loading ppr.o
> start address -T 0x875d4e0 Finished loading ppr.o
> 
> [ 0.0 0.0 0.0 ]
> Finished loading make/compile.lisp
> T
> 
> >
> Suspended
> % echo '"'${LISP}'" "'`pwd`'"' > nqthm-1992-tmp
> % fg
> gcl-2.6.1
> (load "make/save.lisp")
> 
> Loading make/save.lisp
> Loading nqthm.lisp
> Finished loading nqthm.lisp
> Loading sloop.o
> start address -T 0x89999c0 Finished loading sloop.o
> Loading basis.o
> start address -T 0x897e000 Finished loading basis.o
> Loading genfact.o
> start address -T 0x87aaea0 Finished loading genfact.o
> Loading events.o
> start address -T 0x89a5760 Finished loading events.o
> Loading code-1-a.o
> start address -T 0x89f9000 Finished loading code-1-a.o
> Loading code-b-d.o
> start address -T 0x8a5b000 Finished loading code-b-d.o
> Loading code-e-m.o
> start address -T 0x8966000 Finished loading code-e-m.o
> Loading code-n-r.o
> start address -T 0x873bbc0 Finished loading code-n-r.o
> Loading code-s-z.o
> start address -T 0x89d0fe0 Finished loading code-s-z.o
> Loading io.o
> start address -T 0x8992a00 Finished loading io.o
> Loading ppr.o
> start address -T 0x8985fe0 Finished loading ppr.o
> 
> [ 0.0 0.0 0.0 ]
> Loading make/tmp.o
> start address -T 0x87a8f60 Finished loading make/tmp.o
> Finished loading make/save.lisp
> T
> 
> >GCL (GNU Common Lisp)  (2.6.1) Sun Nov 16 04:38:18 CST 2003
> Licensed under GNU Library General Public License
> Dedicated to the memory of W. Schelter
> 
> Use (help) to get some basic information on how to use GCL.
> 
> Nqthm-1992.
> Initialized with (BOOT-STRAP NQTHM) on November 17, 2003  13:02:45.
> 
> 
> >
> Suspended
> % cd /u/boyer/pc-nqthm-1992
> % make clean
> rm -f make/compile-success pc-nqthm-1992 TAGS
> rm -f *.o *.c *.h *.data *.sbin *.lbin *.fasl *.sparcf \
>  make/tiny-test.* *saved_pc-nqthm-1992 make/tmp.* *.log
> % make clean-giant-examples
> cd ./examples ; rm -f */*.lisp */*.lib */*.trans */*.err */*.log \
>   */*.proofs* */*.proved */*.STARTED */tmp.* */*.fail \
>   */*.o */*.fasl */*.lbin */*.sbin */*.sparcf \
>   */*.data */*.c */*.h */[0123456789]*
> % set CMULISP=cmulisp
> % fg
> gcl-2.6.1 (wd: ~/nqthm-2nd/nqthm-1992)
> (SETQ SI::*MULTIPLY-STACKS* 16)
> 
> 16
> 
> >GCL (GNU Common Lisp)  (2.6.1) Sun Nov 16 04:38:18 CST 2003
> Licensed under GNU Library General Public License
> Dedicated to the memory of W. Schelter
> 
> Use (help) to get some basic information on how to use GCL.
> 
> Nqthm-1992.
> Initialized with (BOOT-STRAP NQTHM) on November 17, 2003  13:02:45.
> 
> 
> >(si::chdir "/u/boyer/pc-nqthm-1992")
> 
> "/u/boyer/pc-nqthm-1992"
> 
> >(load "make/compile.lisp")
> 
> Loading make/compile.lisp
> Loading pc-nqthm.lisp
> Loading lisp-test.o
> start address -T 0xde99780 Finished loading lisp-test.o
> Finished loading pc-nqthm.lisp
> Loading proclaim-nqthm.lisp
> Finished loading proclaim-nqthm.lisp
> Loading nqthm-patches.o
> start address -T 0x89bad70 Finished loading nqthm-patches.o
> Loading basis-pc.o
> start address -T 0x87ac000 Finished loading basis-pc.o
> Loading macro-commands-aux.o
> start address -T 0x89bc000 Finished loading macro-commands-aux.o
> Finished loading make/compile.lisp
> T
> 
> >
> Suspended
> (wd now: ~/pc-nqthm-1992)
> % echo '"'${CMULISP}'" "'`pwd`'"' > pc-nqthm-1992-tmp
> % fg
> gcl-2.6.1 (wd: ~/nqthm-2nd/nqthm-1992)
> (load "make/save.lisp")
> 
> Loading make/save.lisp
> Loading pc-nqthm.lisp
> Loading lisp-test.o
> start address -T 0x8a39f20 Finished loading lisp-test.o
> Finished loading pc-nqthm.lisp
> Loading defn-sk.o
> start address -T 0x8989000 Finished loading defn-sk.o
> Loading nqthm-patches.o
> start address -T 0x87b29c0 Finished loading nqthm-patches.o
> Loading basis-pc.o
> start address -T 0x8a3b000 Finished loading basis-pc.o
> Loading help.o
> start address -T 0x87b2c20 Finished loading help.o
> Loading utilities.o
> start address -T 0xe01f000 Finished loading utilities.o
> Loading top.o
> start address -T 0xe05c000 Finished loading top.o
> Loading top-nqthm.o
> start address -T 0xe04d000 Finished loading top-nqthm.o
> Loading macro-commands-aux.o
> start address -T 0xe07a000 Finished loading macro-commands-aux.o
> Loading macro-commands.o
> start address -T 0xe09e000 Finished loading macro-commands.o
> 
> Nqthm-1992 mods:  (PC-NQTHM-1992)
> 
> 
> [ 0.0 0.0 0.0 ]
> Loading make/tmp.o
> start address -T 0x8a4f2e0 Finished loading make/tmp.o
> Finished loading make/save.lisp
> T
> 
> >(si::chdir "examples")
> 
> "examples"
> 
> >(load "dir.lisp")
> 
> Loading dir.lisp
> 
> Loading dir.lisp.
> Evaluating this form: 
> 
> (PROGN
>   (DEFPARAMETER *PC-NQTHM-EXAMPLES-DIR* "./")
>   (DEFPARAMETER *PC-NQTHM-SOURCE-DIR* "../")) 
> Finished loading dir.lisp.
> Finished loading dir.lisp
> T
> 
> >(load "driver.lisp")
> 
> Loading driver.lisp
> 
> Loading driver.lisp.
> We will assume that the Pc-Nqthm-1992 examples directory at this site is: 
> 
>    ./
> 
> We will also assume that the single character / is used to separate
> subdirectory components under this operating system.
> 
> Starting the Pc-Nqthm-1992 examples November 17, 2003  13:03:46.
> Trying subset.events.
> Successfully finished subset.events.
> Trying arith.events.
> Successfully finished arith.events.
> Trying mergesort.events.
> Successfully finished mergesort.events.
> Trying events1.events.
> Successfully finished events1.events.
> Trying transitive-closure.events.
> Successfully finished transitive-closure.events.
> Trying events2.events.
> Successfully finished events2.events.
> Trying pigeon-hole.events.
> Successfully finished pigeon-hole.events.
> Trying hanoi.events.
> Successfully finished hanoi.events.
> Trying ramsey1.events.
> Successfully finished ramsey1.events.
> Trying ramsey2.events.
> Successfully finished ramsey2.events.
> Trying square.events.
> Successfully finished square.events.
> Trying tsquare.events.
> Successfully finished tsquare.events.
> Trying symmetric-difference.events.
> Successfully finished symmetric-difference.events.
> Trying csb.events.
> Successfully finished csb.events.
> Trying finite-state-machine-example.events.
> Successfully finished finite-state-machine-example.events.
> Trying koenig.events.
> Successfully finished koenig.events.
> Trying ramsey.events.
> Successfully finished ramsey.events.
> Trying sets.events.
> Successfully finished sets.events.
> Trying alists.events.
> Successfully finished alists.events.
> Trying terms.events.
> Successfully finished terms.events.
> Trying generalize.events.
> Successfully finished generalize.events.
> Trying c1.events.
> Successfully finished c1.events.
> Trying c2.events.
> Successfully finished c2.events.
> Trying c3.events.
> Successfully finished c3.events.
> Trying c4.events.
> Successfully finished c4.events.
> Trying c5.events.
> Successfully finished c5.events.
> Trying c-signal.events.
> Successfully finished c-signal.events.
> Trying c-prog2.events.
> Successfully finished c-prog2.events.
> Trying c-loop.events.
> Successfully finished c-loop.events.
> Trying c-if.events.
> Successfully finished c-if.events.
> Trying c-begin.events.
> Successfully finished c-begin.events.
> Trying c-predefined1.events.
> Successfully finished c-predefined1.events.
> Trying c-predefined2.events.
> Successfully finished c-predefined2.events.
> Trying c-predefined3.events.
> Successfully finished c-predefined3.events.
> Trying c-predefined4.events.
> Successfully finished c-predefined4.events.
> Trying c-proc-call1.events.
> Successfully finished c-proc-call1.events.
> Trying c-proc-call2.events.
> Successfully finished c-proc-call2.events.
> Trying ca10.events.
> Successfully finished ca10.events.
> Trying r2.events.
> Successfully finished r2.events.
> Trying gf.events.
> Successfully finished gf.events.
> Trying gp.events.
> Successfully finished gp.events.
> Trying ground-resolution.events.
> Successfully finished ground-resolution.events.
> Trying bags.events.
> Successfully finished bags.events.
> Trying naturals.events.start address -T 0x8ea14e0 
> Successfully finished naturals.events.
> Trying interpreter.events.
> Successfully finished interpreter.events.
> Trying dining.events.
> Successfully finished dining.events.
> Trying fifo.events.
> Successfully finished fifo.events.
> Trying me.events.
> Successfully finished me.events.
> Trying min.events.
> Successfully finished min.events.
> Trying Anrd.events.
> Successfully finished Anrd.events.
> Trying bags.events.
> Successfully finished bags.events.
> Trying naturals.events.start address -T 0xe1113c0 
> Successfully finished naturals.events.
> Trying integers.events.start address -T 0xe10d460 start address -T 0xe35f440 
> Successfully finished integers.events.
> Trying knuth-91.events.
> Successfully finished knuth-91.events.
> Trying knuth-91a.events.
> Successfully finished knuth-91a.events.
> 
> All Pc-Nqthm-1992 tests completed successfully.
> 
> real time : 1184.220 secs
> run time  : 1172.130 secs
> 
> Finished loading driver.lisp.
> Finished loading driver.lisp
> T
> 
> >
> 
> 
> 
> 
> 

-- 
Camm Maguire                                            address@hidden
==========================================================================
"The earth is but one country, and mankind its citizens."  --  Baha'u'llah