[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:
=============================================================================
debian/dlopen.in
=============================================================================
(let ((si::*collect-binary-modules* t) ;; Collect a list of names of each
object file loaded
si::*binary-modules*
(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
(remove-duplicates si::*binary-modules* :test (function equal)) ;;
collected here
"saved_acl2" ;; new
image
(format nil "~S" com) ;; run the
build sequence again in this image
;; with
load redirected to initialize
""
nil)))
=============================================================================
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
./configure.
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
- [Gcl-devel] Re: GCL profiling with ACL2,
Camm Maguire <=