[Axiom-developer] Re: 2.7.0 nqthm compile times

[Matt Kaufmann]

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
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:

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.

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