[Gcl-devel] Re: Could you explain the "profiling ACL2" build recipe?

[Camm Maguire]

Greetings!

<address@hidden> writes:

> Camm,


> I am making slow but steady progress toward my goal of being able to
> profile the execution of my ACL2 books.  Previously, I had been able
> to build a profiling gcl.  Thanks to help from you and Matt
> Kaufmann, I can now generate .o's with the right sort of init
> functions, and can build an ACL2 image whose primitives (e.g., those
> files in axioms.lisp, etc.) can be profiled.  However, the profiling
> results still don't include my application ACL2 code.  Note that I
> *can* profile my code if it is "plain old" GCL: I just
> (COMPILER::LINK (list "myfun1.o" "myfun2.o" ...) "MyNewExecutable"),
> start MyNewExecutable, then do the SI::GPROF-START/SI::GPROF-QUIT
> thing.  But, no such luck for my ACL2 code.  

First, we should understand that a limitation of the ld workaround
means that the heap has to be recreated *from scratch* in each
compiler::link.  One can alas not use this mechanism to incrementally
modify a heap with a load/dump/reexecute sequence.  This is one of the
primary reasons I'd like to get pg support, dyn lib support, and
ia64/mips/alpha/hppa support into the standard load/unexec incremental
process seemingly so true to the spirit of lisp.

What this essentially means is that you need to append your "foo.o" to
the list of si::*binary-modules* supplied to compiler::link in
dlopen.lsp, and run it again in profgcl.  It doesn't appear that you
have tried this yet -- if you have and it failed, please let me know.

You should also know that I use this script primarily to build acl2 on
ia64/alpha/mips/hppa, on which we can only load .o files using
dlopen.  There is a limit of 1024 such files, hence I've prevented the
compilation of closures.  You likely need not do this.  I'd still
suggest trying dlopen (with the append) as is first.

> I have been trying to
> use the dlopen.in that you sent me, but perhaps I don't know how to
> use it yet.  Here's the scenario:  I have built a profiling GCL
> 2.6.5 executable, which I'll call profgcl here.  I have an ACL2 2.9
> distribution; my current working directory is its acl2-sources.  I
> start up profgcl, then paste in the dlopen.in that you sent, having
> changed "/usr/share/address@hidden@/" to the appropriate directory
> path.  It runs, and I get an nsaved_acl2.gcl, which I can then use
> to certify the distributed books, etc.  So far so good.  Now, I want
> to add my own object file, myACL2fun1.o, which was compiled via an
> ACL2 CERTIFY-BOOK, using an earlier ACL2 built on top of the
> profiling GCL, with COMPILER::*DEFAULT-SYSTEM-P* set to T.  I want
> to add myACL2fun1.o to the set of files that get ld'ed, so I can
> profile it -- how do I do that?  Please be specific -- I have tried
> a number of things, including setting SI::*BINARY-MODULES* to (list
> "myACL2fun1.o") by hand, and none of them has worked.   

OK, try this:

=============================================================================
(let ((si::*collect-binary-modules* t) ;; Collect a list of names of each 
object file loaded 
      si::*binary-modules*
      (my-modules (list "myACL2fun1.o" "myACL2fun2.o"))  ;; Put your custom 
modules here
      (compiler::*default-system-p* t));; .o files to be linked in via ld
                                       ;; must be compiled with :system-p t
                       
  
  (let ((com (quote    ;; This is a command to build acl2 which will be run 
twice --
                       ;; once in stock gcl, compiling files, loading and 
recording same
                       ;; once in an image which is linked via ld from the 
results of the above
                       ;;   redirecting each load to an initialization of the 
.o file already
                       ;;   linked into the image by ld
              (progn
                (load "init.lsp.ori")
                (let* ((la (find-symbol "LOAD-ACL2" "ACL2"))  ;; 
acl2::load-acl2 doesn't exist at read-time
                       (olf (symbol-function la))
                       (si::*collect-binary-modules* t))      ;; make sure the 
second pass watches for
                                                              ;; .o loads, for 
the purpose of triggering an error
                  (unless (probe-file "axioms.o")             ;; no sense to 
compile twice
                    (funcall (symbol-function (find-symbol "COMPILE-ACL2" 
"ACL2")))
                    (delete-package "ACL2-PC"))               ;; prevent 
package error when loading after compiling 
                  (funcall olf)                               ;; must load-acl2 
to establish the symbols below 
                  (let ((sa (find-symbol "SAVE-ACL2" "ACL2"))
                        (ia (find-symbol "INITIALIZE-ACL2" "ACL2"))
                        (ib (find-symbol "INCLUDE-BOOK" "ACL2"))
                        (ap2f (find-symbol "*ACL2-PASS-2-FILES*" "ACL2"))
                        (ocf (symbol-function 'compiler::compile))
                        (osf (symbol-function 'si::save-system)))
                    (setf (symbol-function 'compiler::compile)     ;; For now, 
run closures interpreted
                          (lambda (x) (symbol-function x)))        ;; At some 
point, could compile saved
                                                                   ;; gazonk 
files without loading (i.e.
                                                                   ;; returning 
interpreted code) on first pass
                                                                   ;; then 
don't compile by load -> initialize
                                                                   ;; on second 
pass.  Cannot load via dlopen
                                                                   ;; more than 
1024 files at once, and this is
                                                                   ;; the only 
relocation mechanism currently
                                                                   ;; available 
on ia64,alpha,mips,hppa
                                                                   ;; On first 
attempt, failure on initizlization of
                                                                   ;; 
acl2_gazonk3558.o
                    (setf (symbol-function la) (lambda () nil))    ;; save-acl2 
calls load-acl2, but we can't load
                                                                   ;; twice 
when initializing in reality.
                    (setf (symbol-function 'si::save-system)       ;; Restore 
all moved functions on save-system
                          (lambda (x)
                            (setf (symbol-function 'compiler::compile) ocf)
                            (setf (symbol-function la) olf)
                            (setf (symbol-function 'si::save-system) osf)
                            (when si::*binary-modules*             ;; Saving 
when a .o has been loaded is a no-no
                              (error "Loading binary modules prior to image 
save in dlopen image: ~S~%"
                                     si::*binary-modules*))
                            (funcall osf x)))
                    (let* ((no-save si::*binary-modules*))         ;; Don't 
call save-system on first pass
                      (funcall (symbol-function sa)
                               (list ia (list 'quote ib) ap2f 
"/usr/share/address@hidden@/") ;; save-acl2
                               nil
                               no-save))))))))
    
    (eval com)                                                       ;; first 
evaluate the command in gcl
    (compiler::link                                                  ;; link in 
the .o files with ld
     (append 
      (remove-duplicates si::*binary-modules* :test (function equal));; 
collected here
      my-modules)                                                    ;; your 
modules here
     "saved_acl2"                                                    ;; new 
image
     (format nil "~S" com)                                           ;; run the 
build sequence again in this image
                                                                     ;; with 
load redirected to initialize
     ""        
     nil)))
=============================================================================

>  Also, the
> comments in dlopen.in indicate that it should be run twice -- does
> that happen automatically, or do I have to paste it in twice.  If it

It happens automatically, once in the (eval com), and then once in the
image produced by compiler::link as supplied in the third argument as
an init string to run.

> is the latter, how exactly do I perform the second run?  Many thanks
> in advance -- solving this problem in as soon as possible is quite
> important to my project.  David Hardin

If you get stuck and want to send me your .lisp, I might have time to
help. 

Take care,

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