[Axiom-developer] Re: 2.7.0 nqthm compile times

[Matt Kaufmann]

Hi, Camm --

My reply is interspersed below.

   Sender: address@hidden
   Cc: address@hidden, address@hidden, address@hidden,
           address@hidden
   From: Camm Maguire <address@hidden>
   Date: 26 Jun 2007 13:25:31 -0400
   X-SpamAssassin-Status: No, hits=-2.3 required=5.0
   X-UTCS-Spam-Status: No, hits=-315 required=200

   Greetings!

   Matt Kaufmann <address@hidden> writes:

   > Hi, Camm --
   > 
   > Here is some feedback with respect to the use of ACL2 on top of GCL,
   > as I see it.
   > 
   > >>    A final question remains of
   > >>    whether or not to actually use ftype declaims if provided.
   > 
   > As you know, in ACL2 we do our own auto-proclaiming of function types.
   > Just to be safe, I think it would be good if there were a way to turn
   > off the auto-proclamation capability, as a way to work around any
   > problems we might encounter, using our own proclaiming instead.  That

   Absolutely.  Currently, the switch is
   compiler::*compiler-auto-proclaim*.  This said, I have not been
   testing with it off for some time, so there is some risk of drift
   here.

Then it would be great if you'd be willing to test the latest ACL2
(currently Version 3.2.1) using compiler::*compiler-auto-proclaim*
off.  Moreover, it would be interesting to know how (also in GCL
2.7.0) the resulting regression time compares with the use of GCL's
auto-proclaim (and I can tell you how to turn off ACL2's auto-proclaim
for that test), and how these both compare with ACL2 regression time
using GCL 2.6.7.

   What I was really thinking of is what to do when it is on, as is the
   default, and the user proclaims something anyway.  Three options --
   compiler override, user override, or use a type-and of the two.

Good question.  For ACL2 I think we'd be content with whichever is
easiest for you.  If you implement compiler override, you could
perhaps print a message saying that the user proclaim has been
ignored, with a suggestion to set compiler::*compiler-auto-proclaim*
to nil if one wants to use the user's type.

   > said, I can imagine you do a signficantly better job than we do, and
   > I'm looking forward to using this new GCL feature!
   > 
   > I imagine that we might avoid 'si::do-recompile entirely with ACL2.
   > Here are some (potentially confused) thoughts:
   > 

   For large systems, it pays to defer any recompilation until the end.
   It appears the only useful hook for this purpose in the cl spec is
   with-compilation-unit.  So I imagine the three following situations:

   1) casual interactive developement use, autoproclamation and
      recompilation at every step, all is safe and optimal.

I think this would be great for ACL2 users.  They already have the
option of avoiding compilation if they are worried about speed.  By
the way, when users invoke ACL2's so-called book certification,
recompilation is unnecessary (redefinition is disallowed); so ACL2
might set si::*disable-recompile* to nil under the hood at such times.

   2) large system compilation, the developers of which don't want to
      fiddle with proclamation -- wrap the compilation in
      with-compilation-unit. 

That's probably what we will do for ACL2 builds using GCL 2.7.0, if
all is well.

   3) True old-school blackbelts who want to proclaim on their own --
      (setq si::*disable-recompile* t compiler::*compiler-auto-proclaim* nil)

We might want to do this with ACL2 if we run into issues, in which
case we'd still like with-compilation-unit to behave reasonably.  I
don't imagine we'd feel any need to try the other alternative just
below.

      or 

      (setq si::*disable-recompile* t) and have the compiler either take
      user overrides or a type-and of the user and the compiler proclaims

   > Regarding leaving things in a safe state: For many years we have told
   > ACL2 users that they redefine functions at their own peril (and, they
   > have to set a flag even to be able to do any redefinition).  So in a
   > sense, that justifies leaving things in an unsafe state when there is
   > redefinition.  But I think that for ACL2, it would be a nice default
   > to leave things in a safe state, even if this means expensive
   > recompilation (presumably by leaving si::*disable-recompile* at nil,
   > if I understand correctly).  As for with-compilation-unit, I think
   > that the important thing is that it leaves things in a safe state
   > provided there is no redefinition.

   OK, so just to clarify, you vote

   1) (si::*disable-recompile* nil) by default, so that default
      interactive use has safe and hopefully optimal recompilation. 

Great.

   2) with-compilation-unit recompiles any source files containing
      functions with detected signature conflicts at the end, but does
      not compile these functions yet another time for the purpose of
      loading into the running image.  (as stated ealier, it is not safe
      to reload the recompiled original source files due to other
      top-level forms therein.)

In short: I think I'd be content to see an error if functions are
redefined within a with-compilation-unit, and maybe that means I'm
fine with your #2 just above.

Longer reply to your #2 just above: Sorry, but I think I'm not
following here.  I believe that with-compilation-unit is invoked when
building ACL2, but not when users define functions in ACL2.  For the
ACL2 build, I just want things fast and as safe as they are today.  If
you're suggesting that the ACL2 build process might be unsafe because
a final recompile is avoided, that would certainly be unfortunate.
But perhaps the missing recompile you mention isn't relevant to ACL2
builds since we do not redefine functions (I think!) during the ACL2
build process.  Hmmm, well we do redefine a few, for example
user-homedir-pathname for GCL 2.7.0 (I think Bob Boyer had a problem
with that), but probably not inside with-compilation-unit.

   Thanks so much for the feedback.

Thank *you* for all this work and for all you've done for GCL!

   I'd also like to know --

   Do you think this is an improvement, or a dangerous complexity?

I assume that by "this" you mean all the GCL auto-proclaim stuff.  In
the case of ACL2, I don't know if this will have much benefit, since
we already do our own limited auto-proclaiming.  It would be
interesting to do some timings of the ACL2 regression suite as
mentioned above.  But the case of ACL2 may well not be representative,
since not only do we already do some auto-proclaiming, but also we are
in perhaps in an unusual position to do so because ACL2 puts syntactic
restrictions on its definitions beyond what are required by Common
Lisp.

   Take care,

Thanks again --
-- Matt
   > 
   > Thanks --
   > -- Matt
   >    Sender: address@hidden
   >    cc: address@hidden, address@hidden,
   >       Matt Kaufmann <address@hidden>, address@hidden
   >    From: Camm Maguire <address@hidden>
   >    Date: 22 Jun 2007 17:41:25 -0400
   >    X-SpamAssassin-Status: No, hits=-2.3 required=5.0
   >    X-UTCS-Spam-Status: No, hits=-315 required=200
   > 
   >    Greetings!
   > 
   >    [ cc'ed to the maxima and axiom lists, as I would greatly appreciate
   >    any user feedback on what they would like (that is practical) in the
   >    forthcoming gcl release.  If this is unwelcome traffic, please let me
   >    know.]
   > 
   >    Robert Boyer <address@hidden> writes:
   > 
   >    > Fantastic.  Thanks so much!
   >    > 
   > 
   >    The above is most appreciated, but I was hoping for a bit more of an
   >    opinion as to where GCL should be heading in this direction, to wit:
   > 
   >    Code calling compiled functions of known signature can be rendered
   >    incorrect if the callee is subsequently compiled to produce a
   >    different signature:
   > 
   >    
=============================================================================
   >    COMPILER>(defun foo (x y z) (list x y z))
   > 
   >    FOO
   > 
   >    COMPILER>(compile 'foo)
   > 
   >    ;; Compiling /tmp/gazonk_13883_1.lsp.
   >    ;; End of Pass 1.  
   >    ;; End of Pass 2.  
   >    ;; OPTIMIZE levels: Safety=0 (No runtime error checking), Space=0, 
Speed=3, (Debug quality ignored)
   >    ;; Finished compiling /tmp/gazonk_13883_1.o.
   >    ;; Loading /tmp/gazonk_13883_1.o
   >     ;; start address -T 0xaa2f80 ;; Finished loading /tmp/gazonk_13883_1.o
   >    #<compiled-function FOO>
   >    NIL
   >    NIL
   > 
   >    COMPILER>(defun bar (x y z zz) (remove zz (foo x y z)))
   > 
   >    BAR
   > 
   >    COMPILER>(compile 'bar)
   > 
   >    ;; Compiling /tmp/gazonk_13883_1.lsp.
   >    ;; End of Pass 1.  
   >    ;; End of Pass 2.  
   >    ;; OPTIMIZE levels: Safety=0 (No runtime error checking), Space=0, 
Speed=3, (Debug quality ignored)
   >    ;; Finished compiling /tmp/gazonk_13883_1.o.
   >    ;; Loading /tmp/gazonk_13883_1.o
   >    ;; start address -T 0x87b2b0 ;; Finished loading /tmp/gazonk_13883_1.o
   >    #<compiled-function BAR>
   >    NIL
   >    NIL
   > 
   >    COMPILER>(bar 1 2 3 1)
   > 
   >    (2 3)
   > 
   >    COMPILER>(setq si::*disable-recompile* t)
   > 
   >    T
   > 
   >    COMPILER>(defun foo (x y z) (coerce (list x y z) 'vector))
   > 
   >    FOO
   > 
   >    COMPILER>(compile 'foo)
   > 
   >    ;; Compiling /tmp/gazonk_13883_1.lsp.
   >    ; (DEFUN FOO ...) is being compiled.
   >    ;; Warning: ret type mismatch in auto-proclamation (CONS T
   >                                                   (CONS T
   >                                                    (CONS T NULL)))(NIL) -> 
*
   > 
   >    ;; End of Pass 1.  
   >    ;; End of Pass 2.  
   >    ;; OPTIMIZE levels: Safety=0 (No runtime error checking), Space=0, 
Speed=3, (Debug quality ignored)
   >    ;; Finished compiling /tmp/gazonk_13883_1.o.
   >    ;; Loading /tmp/gazonk_13883_1.o
   >     ;; start address -T 0x87b540 ;; Finished loading /tmp/gazonk_13883_1.o
   >    #<compiled-function FOO>
   >    NIL
   >    NIL
   > 
   >    COMPILER>(bar 1 2 3 1)
   >    Segmentation violation: c stack ok:signalling error
   >    Error: ERROR "Caught fatal error [memory may be damaged]: Segmentation 
violation."
   >    Fast links are on: do (si::use-fast-links nil) for debugging
   >    Signalled by BAR.
   >    ERROR "Caught fatal error [memory may be damaged]: Segmentation 
violation."
   > 
   >    Broken at BAR.  Type :H for Help.
   >    COMPILER>>:q
   > 
   >    Top level.
   >    COMPILER>(setq si::*disable-recompile* nil)
   > 
   >    NIL
   > 
   >    COMPILER>(si::do-recompile)
   >    Pass1 signature discovery on 1 functions ...
   >    Compiling and loading new source in #<output stream 
"/tmp/gazonk_13883_jvaAQ9.lsp">
   >    ;; Compiling /tmp/gazonk_13883_jvaAQ9.lsp.
   >    ;; End of Pass 1.  
   >    ;; End of Pass 2.  
   >    ;; OPTIMIZE levels: Safety=0 (No runtime error checking), Space=0, 
Speed=3, (Debug quality ignored)
   >    ;; Finished compiling /tmp/gazonk_13883_jvaAQ9.o.
   >    ;; Loading /tmp/gazonk_13883_jvaAQ9.o
   >     ;; start address -T 0x87ff40 ;; Finished loading 
/tmp/gazonk_13883_jvaAQ9.o
   >    done
   >    NIL
   > 
   >    COMPILER>(bar 1 2 3 1)
   > 
   >    #(2 3)
   > 
   >    COMPILER>(defun foo (x y z) (list x y z))
   > 
   >    FOO
   > 
   >    COMPILER>(compile 'foo)
   > 
   >    ;; Compiling /tmp/gazonk_13883_1.lsp.
   >    ;; End of Pass 1.  
   >    ;; End of Pass 2.  
   >    ;; OPTIMIZE levels: Safety=0 (No runtime error checking), Space=0, 
Speed=3, (Debug quality ignored)
   >    ;; Finished compiling /tmp/gazonk_13883_1.o.
   >    ;; Loading /tmp/gazonk_13883_1.o
   >    Pass1 signature discovery on 1 functions ...
   >    Compiling and loading new source in #<output stream 
"/tmp/gazonk_13883_XL6AKh.lsp">
   >    ;; Compiling /tmp/gazonk_13883_XL6AKh.lsp.
   >    ;; End of Pass 1.  
   >    ;; End of Pass 2.  
   >    ;; OPTIMIZE levels: Safety=0 (No runtime error checking), Space=0, 
Speed=3, (Debug quality ignored)
   >    ;; Finished compiling /tmp/gazonk_13883_XL6AKh.o.
   >    ;; Loading /tmp/gazonk_13883_XL6AKh.o
   >     ;; start address -T 0x880a20 ;; Finished loading 
/tmp/gazonk_13883_XL6AKh.o
   >     ;; start address -T 0x887320 ;; Finished loading /tmp/gazonk_13883_1.o
   >    #<compiled-function FOO>
   >    NIL
   >    NIL
   > 
   >    COMPILER>(bar 1 2 3 1)
   > 
   >    (2 3)
   > 
   >    COMPILER>
   >    
=============================================================================
   > 
   >    The existing philosophy is therefore not to let the load of the new
   >    foo complete without executing the recompile.  This has the
   >    disadvantage of compiling functions possibly multiple times, and
   >    fragmenting the contiguous memory space.
   > 
   >    'si::do-recompile has the following behavior at the moment:
   > 
   >       a) if called without an argument, as is done in every loaded
   >       .o file, will 1) do a fast pass1-only signature discovery run
   >       on the out of date functions, 2) will write the necessary
   >       functions to a temporary file, compile and then load it.  Each
   >       function passes through gcc once, but possibly multiple times
   >       only through pass1.  System is left in a safe state, but code
   >       can be recompiled multiple times on subsequent multiple loads.
   > 
   >       b) if called with a non-nil argument, will do the above, but
   >       write the new source to the filespec provided in the argument,
   >       which is compiled but not loaded.  The system is left in an
   >       unsafe state, and implicitly leaves to the user the job of
   >       integrating the freshly compiled source.
   > 
   >       c) if called with a nil argument, will do the pass1 signature
   >       discovery, and collect a list of original source files
   >       containing the recompiled functions.  These files are then
   >       probed for and recompiled if found.  The system is left in an
   >       unsafe state, and implicitly leaves to the user the job of
   >       integrating the freshly recompiled code.  (These files cannot
   >       be automatically reloaded, as they may contain other top-level
   >       forms which are only intended to be executed once.  Given
   >       this, the load was also skipped for the non-nil argument case
   >       in b) by way of symmetry.  A third recompile for automatic
   >       loading purposes (as in a)) is ommitted to save compile time.)
   > 
   >    'with-compilation-unit is as follows:
   > 
   >    (defmacro with-compilation-unit (opt &rest body)   
   >      (declare (optimize (safety 1)))
   >      (declare (ignore opt)) 
   >      `(progn
   >    (let ((*disable-recompile* t))
   >      ,@body)
   >    (do-recompile nil)))
   > 
   >    So at present it leaves the system in an unsafe state to avoid a
   >    second pass through gcc and load for every recompiled function.  If
   >    there are only compile-files and no loads in the unit, no signature
   >    conflict is detected and no recompilation is done.  Only loaded
   >    functions within the unit trigger recompilation at unit end.  This is
   >    somewhat counter to what one might expect from the ansi-doc
   >    definition, given its emphasis on compile-file item deferral.
   > 
   >    Here are some alternatives:
   > 
   >    1) do another pass through gcc followed by a load when passing the nil
   >       argument (or a just a load when passing the non-nil argument) to
   >       leave the system in a safe state at the expense of more compile
   >       time.
   > 
   >    2) Never automatically recompile at load, leaving the safety < 3 user
   >       to the whims of random segfaults, but provide a safety 3 which
   >       eliminates all branch elimination depending on known return
   >       signatures.
   > 
   >    3) Defer auto recompiles to a re-entry of top-level, minimizing the
   >       window of unsafe code execution.
   > 
   >    ...
   > 
   >    Thoughts most appreciated.  Please help me make this serve the needs
   >    of the community.  For those new to this thread, this mechanism
   >    obviates the need for ftype declaims.  A final question remains of
   >    whether or not to actually use ftype declaims if provided.
   > 
   >    Take care,
   > 
   >    -- 
   >    Camm Maguire                                            address@hidden
   >    
==========================================================================
   >    "The earth is but one country, and mankind its citizens."  --  
Baha'u'llah
   > 
   > 
   > 
   > 

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