Re: address@hidden: Re: [Gcl-devel] Re: Profiling [ was Re: lisp reader enhancement ]]

[Matt Kaufmann]

Hi, Camm --

>> 1) I see you can find heap_end in gdb as I'd advised.  Does this mean
>>    your gcl and acl2 have been compiled with debugging enabled?  Gdb
>>    is not reporting (no debugging symbols found) as is typically the
>>    case when inspecting non-debugging executables. You can check by
>>    inspecting the variable compiler::*cc*.  A debugging image has -g,
>>    and optimizing image has -O6 -fomit-frame-pointer.

I don't think debugging was enabled.  Here is some relevant info.

The value of compiler::*cc* in the ACL2 saved image is:

"gcc -c -Wall -DVOL=volatile -fsigned-char -fwritable-strings -pipe"

I built GCL using:

  ./configure '--enable-maxpage=128*1024' '--x-libraries=/usr/X11R6/lib' 
'--x-includes=/usr/X11R6/include'
  make

In the GCL build log, I see calls such as this:

  gcc -c -Wall -DVOL=volatile -fsigned-char -fwritable-strings -pipe -O6 
-fomit-frame-pointer -I/u/acl2/gcl/gcl-2.5.3/o -I../h -I../gcl-tk bitop.c  

I built ACL2 basically the way I always do -- in this case:

  nice make small PREFIX=gcl- LISP=/u/acl2/gcl/gcl-2.5.3/xbin/gcl >& 
make-gcl.log&

I'm running gcc version 2.95.3 on Redhat Linux 7.3.

>> 2) Do you have some roughly analogous command I can run on stock acl2
>>    here to mimick your steps?  I want to double check the profiling
>>    output.  I.e., some cpu consuming step I can run in stock acl2 to
>>    generate a profile which hopefully exercises the same sorts of acl2
>>    functionality you are looking at here.

Any of the ACL2 regression tests should do.  Here's an example.  Work in the
directory books/rtl/rel2/support/ under the ACL2 distribution, which I'm
assuming has already been run through ACL2 (by running make in the books/
directory).  Put a copy of test.lsp in that directory.  Modify that test.lsp by
commenting out

(ld "pkgs.lisp") ; some constant and package definitions

and then replacing

(certify-book "model-eq" ?) ; the main test

by this:

(certify-book "lop3" ?) ; the main test

Then in that directory, run the command I mentioned before, where
".../gcl-saved_acl2" is your ACL2 image:

  (time .../gcl-saved_acl2) < test.lsp >& test.log&

I think the main part of this test, (certify-book "lop3" ?), would take about 9
minutes on a particular machine at UT that is something like a 750MH Pentium 3.
There are much shorter ones, and if you have the books/workshop/ books there
are much longer ones.

Let me know if you want any further info.

-- Matt
   cc: address@hidden
   From: "Camm Maguire" <address@hidden>
   Date: 12 Aug 2003 13:04:21 -0400
   User-Agent: Gnus/5.09 (Gnus v5.9.0) Emacs/21.2
   X-WSS-ID: 1327C19D689671-01-01
   Content-Type: text/plain;
    charset=us-ascii

   Greetings!  OK a more detailed comment to follow, but first two quick
   questions:

   1) I see you can find heap_end in gdb as I'd advised.  Does this mean
      your gcl and acl2 have been compiled with debugging enabled?  Gdb
      is not reporting (no debugging symbols found) as is typically the
      case when inspecting non-debugging executables. You can check by
      inspecting the variable compiler::*cc*.  A debugging image has -g,
      and optimizing image has -O6 -fomit-frame-pointer.

   2) Do you have some roughly analogous command I can run on stock acl2
      here to mimick your steps?  I want to double check the profiling
      output.  I.e., some cpu consuming step I can run in stock acl2 to
      generate a profile which hopefully exercises the same sorts of acl2
      functionality you are looking at here.

   Take care,

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