[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: address@hidden: Re: [Gcl-devel] Re: Profiling [ was Re: lisp reader
From: |
Matt Kaufmann |
Subject: |
Re: address@hidden: Re: [Gcl-devel] Re: Profiling [ was Re: lisp reader enhancement ]] |
Date: |
Tue, 12 Aug 2003 12:25:49 -0500 |
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