Hi -- You can just make your own directory, grab ACL2 from the web as follows
wget http://www.cs.utexas.edu/users/moore/acl2/v3-4/distrib/acl2.tar.gz and then, after extracting with "tar xfz acl2.tar.gz", type make LISP=<path_to_gcl> in your source directory. Actually, if you want to build ACL2 *exactly* as I did, create this script to use for <path_to_gcl> above, where "..." is the appropriate path: #!/bin/sh .../gcl-2.6.8pre/bin/gcl -eval "(defparameter user::*fast-acl2-gcl-build* t)" $* Then you should be able to do the experiment I sent you before. By the way, what I used for "..." just above was /lusr/opt. -- Matt Cc: [email protected], [email protected] From: Camm Maguire <[email protected]> Date: Wed, 25 Feb 2009 20:43:26 -0500 X-SpamAssassin-Status: No, hits=-2.5 required=5.0 X-UTCS-Spam-Status: No, hits=-280 required=165 Greetings, and thanks! And the acl2 source location, and any special build instructions? Take care, Matt Kaufmann <[email protected]> writes: > Forwarding to gcl-devel: > > From: "David A. Kotz" <[email protected]> > Subject: Re: interrupts in 64-bit GCL > To: Matt Kaufmann <[email protected]> > CC: [email protected], [email protected], [email protected] > Date: Wed, 25 Feb 2009 14:10:58 -0600 > > ./configure --prefix=/lusr/opt/gcl-2.6.8pre \ > --disable-statsysbfd --enable-locbfd \ > --enable-ihssize=2097110 \ > --enable-vssize=2097110 \ > --enable-maxpage=524288 \ > --enable-holediv=100 \ > --enable-debug > > > > > Matt Kaufmann wrote: >> Great! Thank you. Dave, if you send me your build instructions, I'll >> forward them along since you're (I'm guessing) not on the gcl-devel >> list, which only allows posts from members. >> >> Thanks -- >> -- Matt >> Cc: [email protected], [email protected], [email protected] >> From: Camm Maguire <[email protected]> >> Date: Wed, 25 Feb 2009 15:03:41 -0500 >> X-SpamAssassin-Status: No, hits=-2.6 required=5.0 >> X-UTCS-Spam-Status: No, hits=-282 required=165 >> >> Greetings! OK, suprisingly enough I think I might have indirectly >> deduced what is going on. It is verifiably independent of SGC, but >> appears related to 64bit only by the enhanced time window possible in >> which to receive SIGINT. >> >> In short, could you please send me (and post to gcl-devel) the >> instructions for rebuilding your source again against a patched gcl >> tree for testing. >> >> This does bring up the legacy gcl signal handling code, which is quite >> clever given the age in which it was developed, but has since been >> made somewhat obsolete by recent system developments, at least on >> Linux. >> >> The GCL strategy is to maintain global variables tracking pending and >> blcked signals, and to loop over alarm(1) until the unblocking code >> snippet is executed. (i.e. BEGIN_NO_INTERRUPT and END_NO_INTERRUPT, >> which essentially set signals_allowed to 0 and restores the previous >> value respectively). Nowadays, bracketing the code needing protection >> directly with sigprocmask is more typical. Heaven knows what >> portability issues are involved in making this change. >> >> The bug appears to be that critical GC code is not protected against >> interrupts and subsequent possible longjumps. Specifically, >> add_page_to_freelist is apparently allowing partially initialized >> freelists to escape. An immediate fix would be at hand in this case, >> but more systematically we need to review the areas this protection is >> required and come up with a decent centralization policy. I don't >> think there is any reason to clock signals other that object creation, >> gc, and anything modifying tm_table. Other thoughts most welcome. >> >> Take care, >> >> >> >> Matt Kaufmann <[email protected]> writes: >> >> > Hi -- >> > >> > I was able to reproduce the error after building ACL2 a new debug copy >> > of 64-bit gcl that the sysadmins built. Same instructions as before, >> > except for a slight change in the ACL2 executable directory. Quoting >> > from below, but updating the executable path (and fixing a misleading >> > comment): >> > >> > Start up ACL2 built on GCL, as follows: >> > >> > /projects/acl2/v3-4-linux-64/fast-linux-gcl-saved_acl2 >> > >> > Then issue these commands: >> > >> > ; Just to slow down the output from the thm form below: >> > (trace$ rewrite) >> > >> > ; ACL2 disables the debugger by default; this restores it: >> > (set-debugger-enable t) >> > >> > ; This goes pretty fast but you'll have time to interrupt it: >> > (thm (equal (append (append x x) x) (append x x x))) >> > >> > [Now quickly interrupt with control-c, and then :q from the break. >> > If the form above completes, just try it again. Eventually I think >> > you'll see a Lisp "fatal error" or even a "Segmentation fault".] >> > >> > It seems to take me about 3 to 5 THM calls to get the error, which >> > looks like this: >> > >> > ACL2 !>(thm (equal (append (append x x) x) (append x x x))) >> > [SGC off] >> > Error: Caught fatal error [memory may be damaged] >> > Fast links are on: do (si::use-fast-links nil) for debugging >> > Error signalled by ACL2_*1*_ACL2::THM-FN. >> > Broken at COND. Type :H for Help. >> > ACL2[RAW LISP]>> >> > >> > -- Matt >> > Date: Mon, 23 Feb 2009 17:12:04 -0600 >> > From: "David A. Kotz" <[email protected]> >> > CC: [email protected], [email protected], [email protected] >> > >> > I've replaced both of our 64bit flavors and the 32bit with debug-enabled >> > versions. The 64s are in place now, and the 32 should rdist around >> > tonight. I want to keep all of them in sync, even if we're only >> > investigating a problem in one. >> > >> > - dave >> > >> > >> > Matt Kaufmann wrote: >> > > Thanks, Dave! I really appreciate it. >> > > >> > > When I get the word from you, or when I see >> > > /lusr/opt/gcl-2.6.8pre/bin/gcl updated on lhug-0, I'll rebuild ACL2 on >> > > top of it and try to reproduce the problem. >> > > >> > > Thanks again -- >> > > -- Matt >> > > Date: Mon, 23 Feb 2009 10:13:54 -0600 >> > > From: "David A. Kotz" <[email protected]> >> > > CC: Matt Kaufmann <[email protected]>, [email protected], >> > > [email protected] >> > > >> > > I'll rebuild it with the debug flag. >> > > >> > > - dave >> > > >> > > >> > > Camm Maguire wrote: >> > > > Thanks! Please let me know if you run into troubles here. >> > > > >> > > > Take care, >> > > > >> > > > Matt Kaufmann <[email protected]> writes: >> > > > >> > > >> Howdy -- >> > > >> >> > > >> Thanks for the reply. >> > > >> >> > > >> If gr...@cs is willing to do (1), or to send me the exact configure >> > > >> and make commands and source directory used so that I can do it >> > > >> myself, then I'll try to reproduce the error by building ACL2 on top >> > > >> of it. I'm assuming that --enable-debug is given to the configure >> > > >> command, not to make. >> > > >> >> > > >> Then if if I can't reproduce the problem, I'll let you and gr...@cs >> > > >> know and we can explore (2). In that case, if gr...@cs is willing to >> > > >> do it, great; then I'll try to reproduce the problem. But if I'm to >> > > >> do the build, I'd need explicit instructions on how to "make sure -g >> > > >> is included in the gcc calls"; maybe I need to do some setq in Lisp? >> > > >> Also I didn't understand the comment about makedefs. But I guess we >> > > >> can ignore (2) if (1) works. >> > > >> >> > > >> -- Matt >> > > >> Cc: [email protected], [email protected] >> > > >> From: Camm Maguire <[email protected]> >> > > >> Date: Fri, 20 Feb 2009 20:58:49 -0500 >> > > >> X-SpamAssassin-Status: No, hits=-2.6 required=5.0 >> > > >> X-UTCS-Spam-Status: No, hits=-282 required=165 >> > > >> >> > > >> Greetings! I suspect a missing signal block around some code that >> > > >> needs protecting. I've reprodced under gdb, but there are no >> > > >> debugging symbols in the image. [ Question for list -- have computers >> > > >> now become so fast that -g should be included by default in all gcl >> > > >> images? It used to slow down the compiler, don't know about now. It >> > > >> does make the image quite a bit bigger. ] >> > > >> >> > > >> Ideally, you or someone else at the site might be so kind as to >> > > >> rebuild atop >> > > >> >> > > >> 1) a gcl build with --enable-debug. If this does not reproduce, then >> > > >> in addition >> > > >> 2) rebuild atop a standard gcl with the CFLAGS environment variable >> > > >> set to -g before configure and make. Please make sure -g is included >> > > >> in the gcc calls. Otherwise, makedefs can be modified after configure >> > > >> and before make to include -g wherever one sees -O3 or -O >> > > >> >> > > >> Would this be too much trouble? >> > > >> >> > > >> Take care, >> > > >> >> > > >> Matt Kaufmann <[email protected]> writes: >> > > >> >> > > >> > Hi -- >> > > >> > >> > > >> > The sysadmins here at UT CS have built GCL 2.6.8pre from CVS as you >> > > >> > suggested. It's working great on 32-bit linux, but I've run into an >> > > >> > issue for 64-bit linux. >> > > >> > >> > > >> > You can re-create the issue on a UT CS 64-bit linux machine as >> > > >> > follows. >> > > >> > >> > > >> > Start up ACL2 built on GCL, as follows: >> > > >> > >> > > >> > /projects/acl2/v3-4-linux/fast-linux-gcl-saved_acl2 >> > > >> > >> > > >> > Then issue these commands: >> > > >> > >> > > >> > ; Just to slow down the output from the next form: >> > > >> > (trace$ rewrite) >> > > >> > >> > > >> > ; ACL2 disables the debugger by default; this restores it: >> > > >> > (set-debugger-enable t) >> > > >> > >> > > >> > ; This goes pretty fast but you'll have time to interrupt it: >> > > >> > (thm (equal (append (append x x) x) (append x x x))) >> > > >> > >> > > >> > [Now quickly interrupt with control-c, and then :q from the break. >> > > >> > If the form above completes, just try it again. Eventually I think >> > > >> > you'll see a Lisp "fatal error" or even a "Segmentation fault".] >> > > >> > >> > > >> > By the way, I built /projects/acl2/v3-4-linux/fast-linux-gcl as >> > > >> > follows, on lhug-0 (a 64-bit linux machine): >> > > >> > >> > > >> > rm -f TAGS ; mv make-fast-gcl.log make-fast-gcl.old.log ; (time nice make PREFIX=fast-linux-gcl- LISP=my-fast-gcl) >& make-fast-gcl.log& >> > > >> > >> > > >> > where "my-fast-gcl" is a script containing: >> > > >> > >> > > >> > #!/bin/sh >> > > >> > /lusr/opt/gcl-2.6.8pre/bin/gcl -eval "(defparameter user::*fast-acl2-gcl-build* t)" $* >> > > >> > >> > > >> > Also by the way, if you instead run the following on a 32-bit UT CS >> > > >> > linux machine >> > > >> > >> > > >> > /projects/acl2/v3-4-linux/gcl-saved_acl2 >> > > >> > >> > > >> > then you won't see the interrupt problem described above (or at least, >> > > >> > I didn't, and I tried). >> > > >> > >> > > >> > Thanks -- >> > > >> > -- Matt >> > > >> > >> > > >> > >> > > >> > >> > > >> > >> > > >> >> > > >> -- >> > > >> Camm Maguire [email protected] >> > > >> ========================================================================== >> > > >> "The earth is but one country, and mankind its citizens." -- Baha'u'llah >> > > >> >> > > >> >> > > >> >> > > >> >> > > > >> > >> > >> > >> > >> >> -- >> Camm Maguire [email protected] >> ========================================================================== >> "The earth is but one country, and mankind its citizens." -- Baha'u'llah > ---------- > -- Camm Maguire [email protected] ========================================================================== "The earth is but one country, and mankind its citizens." -- Baha'u'llah _______________________________________________ Gcl-devel mailing list [email protected] http://lists.gnu.org/mailman/listinfo/gcl-devel
