[Top][All Lists]

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Gcl-devel] Re: GCL profiling with ACL2

From: Camm Maguire
Subject: [Gcl-devel] Re: GCL profiling with ACL2
Date: 20 Mar 2005 09:01:11 -0500
User-agent: Gnus/5.09 (Gnus v5.9.0) Emacs/21.2

Greetings!  Hopefully I can provide more detail later -- time is a bit
short at the moment.

1)  The current code for building ACL2 in the .text section of the
    final executable, as opposed to the default .data section, and
    which is a prerequisite at present for having acl2 functions
    visible to gprof, is:

(let ((si::*collect-binary-modules* t) ;; Collect a list of names of each 
object file loaded 
      (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
                (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" 
                    (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
                    (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~%"
                            (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
    (eval com)                                                       ;; first 
evaluate the command in gcl
    (compiler::link                                                  ;; link in 
the .o files with ld
     (remove-duplicates si::*binary-modules* :test (function equal)) ;; 
collected here
     "saved_acl2"                                                    ;; new 
     (format nil "~S" com)                                           ;; run the 
build sequence again in this image
                                                                     ;; with 
load redirected to initialize

        As the name implies, this is found in the debian ACL2 package
        source package with the above pathspec.  It is an 'in' file,
        which means it is processed by autoconf or the like --
        effectively this just means that you should substitute the
        @VR@ string above for the current version of acl2

2) In addition, your GCL image needs to have profiling support.  This
   should be indicated in the startup banner with the simple word
   'profiling'.  On Debian systems (only to my knowledge), the gcl
   binary package contains all four gcl images, CLtL1, ANSI, CLtL1
   profiling, and ANSI profiling, which are runtime selectable with the
   environment variables GCL_ANSI and GCL_PROF (defaults are also set
   a package installation time).  On other systems, on when building
   gcl by hand, you need to add the --enable-gprof option to

3) As you note in the above build script, compilations need to proceed
   with the :system-p flag set for profiling -- the above code does
   this for you.  This flag essentially has three effects -- the
   initialization function for the file is called init_<file> instead
   of init_code, '#include "cmpinclude.h' is put at the head of the C
   output file instead of the text of compiler::*cmpinclude-string*,
   and the initialization 'data' (lisp init code actually) which is
   appended to the .o file is written in human readable form instead
   of its byte compiled 'fasd' form.  The idea is that this flag is
   appropriate for GCL's lisp files themselves, where cmpinlcude.h is
   readily available, where one wants to see the lisp data code for
   debugging, and where one typically makes 'raw' images as a
   preliminary step in the build not via si::save-system, but as
   output directly by ld itself, which requires all functions to have
   a unique name.  

   The reason I mention this is that these three are actually
   separately manipulable.  :system-p t directly effects the C init
   function name, compiler::*fasd-data* can separately govern the lisp
   init code format, and one can bind compiler::*cmpinclude-string* to
   nil if one always wants the shorter '#include "cmpinclude.h"'.  we
   might use and extend this in the future to make the default more
   sane.  *cmpinclude-string* is huge and bloats the output C file,
   but doesn't effect the output .o file size of course, and has the
   advantage of being completely portable.  Perhaps on modern systems
   rewriting this large data over and over for each C file is simply
   better.  *fasd-data* should also likely always be set to t
   regardless of system-p.  Likewise, always having a variable C init
   function name is likely a good idea, defaulting to
   init_function_name rather than init_filename when using compile
   instead of compile-file, as it should handle both the interactive
   and batch cases equally.

   As for the path to cmpinclude.h, this should be handled for you
   automatically, as the compiler appends -I si::*system-directory*
   ../h to the gcc command line.  Perhaps you could investigate your
   si::*system-directory* variable.

4) As you know, profiling is governed by sandwiching your code between
   (si::gprof-start) and (si::gprof-quit).

5) You can likely stop reading here, but I'm including some thoughts
   for further development here for the purposes of gcl-devel.
   compiler::link is a distinctly non-lisp ugly but necessary
   work-around.  Unlike si::save-system, it does not preserve any
   state of the image, but gives one a fresh image made only by
   running the lisp init code of the included object files.  We need
   it currently in three cases: a) profiling, b) building at all on
   systems which cannot yet natively relocate .o files (ia64, mips,
   mipsel, hppa, and alpha), and c) when wanting permanently link the
   image to a new external C library, particularly a shared library.
   All three of these limitations can be overcome with a certain
   amount of low level work.  a) extend fasload and unexec to load,
   merge, and save the profiling sections emitted by gcc's -pg flag,
   b) write bfd or sfaslelf routines for the missing arches using lush
   as an example, and c) bringing forward dlopen to the lisp level,
   maintaining a list of symbols used therein by loaded .o files, and
   extending unexec again to add reloc records to the output image.
   all of this would take a finite but non-trivial amount of time, but
   I feel would make gcl a better product.

6) Another approach to the profiling functionality would be to forgo
   gprof in favor of Dr. Schelter's 'profile' lisp function support.
   See the info pages for this.  The big issue here is that the profile
   is flat -- no call graph.  It may be easier to reimplement gprof in
   lisp or GCL's C, however, than to manipulate the fasload and unexec
   functions as described above.

Sorry this ha gotten so long.  Please don't hesitate to ask for
clarification if needed.

Take care,

Matt Kaufmann <address@hidden> writes:

> Hi, Camm --
> [I'm including Bob Boyer because Bob, I think you've done some profiling with
> GCL.]
> You might have seen the email I just sent to David Hardin's acl2-help query.
> The bottom line is that he wants to do profiling with ACL2 built on GCL.  I
> think that GCL 2.6.6 already is set up for profiling if ACL2 is built using
> compiler::link, if I start with with environment variable GCL_PROF set to any
> non-empty string.  Is that right?  I believe that capabilility exists in GCL
> 2.6.5 too; how far back does it go?  And I think ACL2 would need to be built
> with compiler::link, and you already have makefile (and perhaps other) support
> for this.
> Perhaps you don't actually have a Makefile modification.  Sometime ago you 
> sent
> me the following.  Is this still basically what you would do to build a
> profiling-enabled ACL2 image?
> mv init.lsp init.lsp.ori
> echo '(setq compiler::*default-system-p* t compiler::*default-c-file* t)' 
> >foo.lsp
> echo '(load "foo.lsp")(in-package "acl2")(compile-acl2)' | gcl
> echo '(load "foo.lsp")(in-package "acl2")
>         (load-acl2)(initialize-acl2 (quote include-book) *acl2-pass-2-files* 
> t t)' | gcl
> echo '(compiler::link 
>         (list "acl2-fns.o" 
>               "axioms.o" 
>               "basis.o" 
>               "translate.o" 
>               "type-set-a.o" 
>               "type-set-b.o" 
>               "rewrite.o" 
>               "simplify.o" 
>               "bdd.o" 
>               "other-processes.o" 
>               "induct.o" 
>               "history-management.o" 
>               "prove.o" 
>               "defuns.o" 
>               "proof-checker-a.o" 
>               "defthm.o" 
>               "other-events.o" 
>               "ld.o" 
>               "proof-checker-b.o" 
>               "tutorial.o" 
>               "interface-raw.o" 
>               "linear-a.o" 
>               "linear-b.o" 
>               "non-linear.o" 
>               "TMP1.o") 
>               "nsaved_acl2" 
>               "(load \"foo.lsp\") 
>                (setq compiler::*default-system-p* nil)
>                (in-package \"acl2\")
>                (save-acl2 (quote (initialize-acl2 
>                         (quote include-book) *acl2-pass-2-files* t nil
>                         \"/usr/share/acl2-2.8/books/\")) 
>                         \"saved_acl2\"))" "" nil)' | gcl
> If I'm correct above, then I think it would be easy to update the ACL2
> distribution so that users can do a new "make gprof" build of ACL2 on top of
> GCL that allows profiling.  The new gprof target would essentially be the
> target you use to do a build with compiler::link (or if there isn't one yet,
> then a target based on the code displayed above), where we set environment
> variable GCL_PROF to "true" (say) before starting GCL.  Is it necessary to set
> compiler::*default-c-file* to t in order for profiling to work?
> Does this seem reasonable?  If so, and if you're willing for me to modify the
> ACL2 makefile based on your compiler::link ACL2 makefile code (or the code
> above), I'd appreciate your sending me the latest version of your code for
> this.
> If you have any simple user-level documentation for doing profiling, that 
> would
> be great too.  By analogy, if I were writing such documentation for Allegro I
> might simply say something like this:
> (prof:start-profiler)  ; start profiling
> (prof:show-call-graph) ; start profiling
> (prof:stop-profiler)   ; stop profiling
> Of course, if there is any more thorough documentation out there, that would 
> be
> good to know about, too.
> Thanks!
> -- Matt

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

reply via email to

[Prev in Thread] Current Thread [Next in Thread]