Hi, Camm --
That's exciting that GCL, which is already the fastest Lisp I know of
for running ACL2, may become even faster! Thank you.
I don't have any opinions about defaults or heuristics, but:
It might be *very* useful to have a user-settable special variable
that controls inlining. I'm imagining that by default, ACL2 would
inline all built-in and user-defined function calls that GCL allows,
but that when one wants to trace, then it would be nice to be able to
rebuild with inlining turned down or off.
Thanks --
-- Matt
cc: boyer at cs.utexas.edu, Matt Kaufmann <kaufmann at cs.utexas.edu>,
daly at axiom-developer.org, axiom-developer at nongnu.org,
"Robert Dodier" <robert.dodier at gmail.com>,
Maxima mailing list <Maxima at math.utexas.edu>
From: Camm Maguire <camm at enhanced.com>
Date: Fri, 06 Jul 2007 12:58:02 -0400
X-SpamAssassin-Status: No, hits=-2.5 required=5.0
X-UTCS-Spam-Status: No, hits=-280 required=200
Greetings! If you would be so kind, I'd appreciate some direction on
the desired inlining policy fro gcl 2.7.0.
GCL has always inlined certain functions, e.g. mapcar, member, etc.
Without this, performance would be noticeably worse.
Traditionally, this has been accomplished though ad-hoc 'c1 functions
in the compiler, or C-snippet inline attributes in cmpopt.lsp. Thus
one had not only to write the function, but its inline support in the
compiler as well. Support for these remain, but thanks to Boyer's
suggestion to carry the original source around in the image, automatic
inlining is now possible. Support for this is in place in 2.7 with
notable improvements in performance.
The question is, what functions should be inlined by default?
Currently, symbols external to the lisp package are automatically
considered. Explicitly declared or declaimed functions are also.
inlining may decline if the inline is too large, using a heuristic
function using the *space* setting as input, though in many cases,
inlined code is smaller. The real cost of inlining is compiler speed,
and tracing support.
Boyer recently posted a benchmark which would benefit greatly from
automatic inlining of user functions.
Separately, should inlining be allowed at safety 3?
Take care,
--
Camm Maguire camm at enhanced.com
==========================================================================
"The earth is but one country, and mankind its citizens." -- Baha'u'llah