gcl-devel
[Top][All Lists]
Advanced

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

[Gcl-devel] Re: gcl profiler?


From: Camm Maguire
Subject: [Gcl-devel] Re: gcl profiler?
Date: 13 Jul 2004 18:15:53 -0400
User-agent: Gnus/5.09 (Gnus v5.9.0) Emacs/21.2

Greetings! Matt, please forward to acl2-help if you think it is
useful.

First, let me please state that we've just added gprof support
natively in gcl.  Useful timings and graphs are definitely attainable
at present, but the user interface can definitely use some work.  If
you find this useful, perhaps feedback from you and others can help us
improve the ease of use.


"Eric W. Smith" <address@hidden> writes:

> Camm and Matt,
> 
> Thanks for the info on this!  Unfortunately, I think I still need some help.  
> I
> understand that I need to rebuild gcl with gprof enabled, but after that 
> things
> get fuzzy.  How do I build a version of ACL2 in which 1) all of the ACL2
> functions are compiled into the .text section and 2) C files are kept around? 

Here is how I do this on Debian:
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

> Right now, I just type "make LISP=gcl" to make ACL2.  I guess I'd need to edit
> the Makefile?
> 
> (BTW, would either of 1) and 2) be cheap enough to just do it by default?)
> 

Yes, there is no performance penalty for these.

> Also, I will want to profile my own functions (e.g., metafunctions).  How 
> would
> I tell ACL2 to do 1) and 2) above for my own functions as well?
> 

The basic idea is to add your compiled objects (.o files) to the list
in compiler::link above.

If you are interested, and especially if you can help with some ideas,
I will explain the difficulty in getting profiling information from
compiled modules conventionally loaded into the .data section in the
traditional build process.

Take care,

> To entice you guys to help with this, I'll point out that someone else on the
> acl2-help list just posted another question about profiling ACL2 when built
> with gcl, and I'll offer to send you guys the results of the profiling 
> (subject
> to approval by my boss), in case they highlight any potentially slow pieces of
> code. 
> 
> Thanks!
> -Eric
> 
> 
> 
> 
> 
> --- Camm Maguire <address@hidden> wrote:
> > Greetings!  Yes there are two profiling capabilities in GCL, based on
> > profil and gprof respectively, the latter giving the more extensive
> > output.  Gprof support needs to be selected at compile time with
> > --enable-gprof.  It is not enabled by default due to the extra memory
> > consumption.  Then just bracket your stuff between (si::gprof-start)
> > and (si::gprof-quit).  Presumably you want information not just on
> > time spent in GCL core functions, but also in your compiled lisp
> > code.  These functions need to be compiled into the .text section of
> > the executable in order to be reported, which one achieves via
> > 
> > (compiler::link (list "my_obj1.o" "my_obj2.o") "new_image")
> > 
> > Fire up new_image, and bracket the calls between gprof-start and
> > gprof-quit as described above.  Compiled lisp functions are given
> > arbitrary names, e.g. L1(), etc.  Each function has a comment in the C
> > source giving its lisp name.  So when compiling your objects, keep the
> > generated C by (setq compiler::*default-c-file* t) or use :c-file t as
> > a compile-file argument.  One of the todo items for the next release
> > is to include the lisp function name in the C function name for this
> > reason, as well as to hopefully enable gprof by default if the memory
> > usage can be worked out, and to see if profiling can be done when
> > modules are loaded into the .data section of the executable via (load
> > "my_obj1.o")
> > 
> > Take care,
> > 
> > "Matt Kaufmann" <address@hidden> writes:
> > 
> > > Eric --
> > > 
> > > I think I've profiled with GCL and I might be able to find notes on that,
> > but
> > > this may have changed anyhow now that you're using 2.6.2 (I think).  Camm
> > is on
> > > acl2-help and he may know this stuff cold, so perhaps he'll answer.  If 
> > > you
> > > don't get an answer from him by the time you need it, ping me and I'll see
> > what
> > > I can do.
> > > 
> > > Camm, if you send notes then I may put them on the ACL2 installation page
> > for
> > > the next release, if you don't mind.
> > > 
> > > -- Matt
> > >    Date: Mon, 12 Jul 2004 08:46:46 -0700 (PDT)
> > >    From: "Eric W. Smith" <address@hidden>
> > >    Reply-to: address@hidden
> > >    Sender: address@hidden
> > >    X-Listprocessor-Version: 8.2.10/020311/17:52 -- ListProc(tm) by CREN
> > >    X-WSS-ID: 6CEC6D26880668-01-01
> > >    Content-Type: text/plain;
> > >     charset=us-ascii
> > >    X-Spam-Status: No, hits=0 required=5 tests=
> > >    X-Spam-Level:  
> > >    X-Scanned-By: MIMEDefang 2.39
> > > 
> > >    Does gcl have a profiler?  I'd like to know where the time for my 
> > > proofs
> > is
> > >    going?.  (For example, how fast are my metafunctions?)  Has anyone
> > profiled
> > >    ACL2 using gcl (maybe using gprof?)?
> > > 
> > >    Thanks!
> > >    -Eric
> > > 
> > > 
> > > 
> > > 
> > 
> > -- 
> > 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




reply via email to

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