[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[Gcl-devel] Re: ACL2 in Java
[Gcl-devel] Re: ACL2 in Java
06 Jun 2005 11:58:08 -0400
Gnus/5.09 (Gnus v5.9.0) Emacs/21.2
Peter Dillinger <address@hidden> writes:
> Before you guys get too far along this with this idea, my most recent
> reply to Camm explianed that our goal for this is an ACL2 plugin for
> Eclipse. To fit into the Eclipse framework, the plugin must be able
> to be dynamically loaded and unloaded while Eclipse is running.
> Clearly, the Eclipse Java application (slow enough as it is) has to be
> the "parent" of all of this. That's why I want to be able to run a
> LISP library from Java.
> >From Camm's comment, the shared library approach sounds reasonable, if
> the JVM and LISP system can play nice together. I'm not worried about
> overhead of the loader manipulating addresses--which is a one time
> cost, right?
Yes, and what's more, this in principle can be eliminated via
prelink. The problem really is that most linking in GCL is done
> However, most interactions with ACL2 would be to query "the world," so
> a slow/heavy connection to ACL2 suffices if the Java code can maintain
> a coherent database of "the world". Regardless, the plugin will
> need notions of entities in "the world" (rules, events, definitions,
> etc.) to provide its rich, semantically-aware interface. The hard
> part in implementing such a strategy, therefore, would be efficiently
> maintaining coherency between ACL2 and the plugin (i.e. ACL2 reveals
> everything about changes to environment). A drawback of this approach
> would be that two full instances of "the world" are active in memory
> at the same time, but this shouldn't be more than 10-20MB, right?
Don't know about the size issues, but a socket/pipe IPC surely would
not be less efficient than trying to combine two separate memory
management units (GCL and JVM). Unless one can be turned off, one
will get serious memory overhead regardless.
> With this strategy, a simple pipe/socket interface or something like
> jLinker would be fine.
Just to clarify the earlier post, in principle a shared library GCL is
quite doable, though would require more work than I have time for
right now. The first easy parts are to throw -fPIC onto
compiler::*cc* and "-shared" onto compiler::*ld*, and then to build
your acl2 following the profiling pattern using compiler::link in the
latest acl2 distribution. I would suggest first passing nil as the
last argument to compiler::link and passing an empty string as the
third argument, and then arranging to run the initialization sequence
normally invoked by the third argument at runtime when the load
address is known. This could slow down the load quite a bit. The
other option is to dump the heap in a file somewhere and mmap it after
the acl2 library is loaded. Eventually, one would likely try to
append a preinitialized heap to the .so so at least the relative
offsets are constant. Next, one would likely have to emulate sbrk to
point to a mini-allocator or preassigned extra heap space at the end
of this dumped file. I'm pretty sure the heap will have to be
contiguous, so if one didn't do this, one would try to sbrk/load the
preinitialized heap as usual on the .data section end, and leave sbrk
alone. Lastly, rename main() to main_ori(), and rework to call the
init functions in one go. The interface you'd use would follow the
following line in main():
There are a variety of such hooks in the base C code through which you
can invoke lisp functions externally.
Alas, there is no detailed documentation other than by looking at how
GCL is put together. I'd be happy to answer any specific questions.
If you do go this route, please consider contributing back your
changes/knowledge to the GCL project for the use of others in the
> -peter d
>  http://www.gnu.org/software/kawa/
>  http://sourceforge.net/projects/jatha/
>  http://www.franz.com/support/documentation/6.2/doc/jlinker.htm
> On Sat, Jun 04, 2005 at 07:01:48AM -0500, J Strother Moore wrote:
> > Hi Hanbing. As the author of the M6 model, you're the
> > JVM-in-ACL2 expert. What do you think of this idea? I
> > presume we'd have to implement some of the GUI related API
> > native methods. We'd probably have to make the state in M6
> > be a stobj for efficiency. This project would be a good
> > demonstration of the utility of a formal model! Do you
> > think its practical?
> > J
> > PS Nice idea Bob!
> > ------- Start of forwarded message -------
> > Date: Sat, 4 Jun 2005 06:35:27 -0500
> > From: Robert Boyer <address@hidden>
> > To: address@hidden
> > Cc: address@hidden, address@hidden, address@hidden,
> > address@hidden
> > Subject: Java
> > > We are looking at building a Java frontend for ACL2, but the frequency and
> > > magnitude of interaction (e.g. browsing the logical universe) is such that
> > > a lightweight interface (i.e. no IPC) between Java and LISP would be
> > > ideal.
> > That IPC is a big problem. Here is one possible approach: write an
> > extremely
> > efficient Java byte code interpreter in Lisp and thereby simulate JAVA
> > within
> > Lisp/ACL2. Given the serious work that has gone into getting and checking
> > an
> > ACL2 specification of JAVA byte code, this might be a reasonable sized
> > project. Assuming you have a Java compiler written in Java, you could
> > thereby utterly eliminate Inter Process Communication costs. It is probably
> > the case that you could get maximal efficiency by the approach I mention,
> > especially if you limited your portability by restricting yourself to
> > GCL/Gnu-Linux and perhaps permitted yourself to write a few lines of C for
> > the most critical code.
> > Bob
> > "We were after the C++ programmers. We managed to drag a lot of them
> > about
> > halfway to Lisp." - Guy Steele
> > -
> > -------------------------------------------------------------------------------
> > >From address@hidden Fri Jun 3 10:36:o03 2005
> > Return-Path: <address@hidden>
> > Received: from intech19.enhanced.com (h-66-134-96-17.phlapafg.covad.net
> > [22.214.171.124])
> > by cs.utexas.edu (8.13.4/8.13.4) with ESMTP id j53FZqJG011297;
> > Fri, 3 Jun 2005 10:35:53 -0500 (CDT)
> > Received: from camm by intech19.enhanced.com with local (Exim 3.35 #1
> > (Debian))
> > id 1DeECj-0003GQ-00; Fri, 03 Jun 2005 11:35:25 -0400
> > To: Peter Dillinger <address@hidden>
> > Cc: Panagiotis Manolios <address@hidden>, address@hidden,
> > address@hidden, address@hidden
> > Subject: Re: using gcl to create shared library?
> > References: <address@hidden>
> > From: Camm Maguire <address@hidden>
> > Date: 03 Jun 2005 11:35:24 -0400
> > In-Reply-To: <address@hidden>
> > Message-ID: <address@hidden>
> > Lines: 60
> > User-Agent: Gnus/5.09 (Gnus v5.9.0) Emacs/21.2
> > MIME-Version: 1.0
> > Content-Type: text/plain; charset=us-ascii
> > X-SpamAssassin-Status: No, hits=-2.6 required=5.0
> > X-UTCS-Spam-Status: No, hits=-322 required=180
> > Greetings!
> > While this would be possible, I think the natural direction would be
> > to call the GUI as an embedded external rather than the other way
> > around. There are several options in this area. Check out gcl-tk,
> > and if you do, use branch 2.6.7pre from cvs (-r Version_2_6_7pre).
> > Also, Mike Thomas has a japi java gui interface option, try
> > - --enable-japi to configure.
> > There appears to be more demand on having GCL manage more resources
> > rather than fewer, so the embedded approach while possible is likely
> > to collide with these other considerations. Not the least of which is
> > that GCL natively loads and relocates its own object modules at fixed
> > address offsets -- loading in a shared library would have to
> > gurarantee the same load address unless we use dlopen as the dynamic
> > linker (--enable-dlopen), which is quite limited in comparison -- one
> > cannot preserve loads across image saves, no more than 1024 open file
> > descriptors, etc.
> > Can java run embedded under lisp?
> > Please keep us posted!
> > Take care,
> > Peter Dillinger <address@hidden> writes:
> > > I'm working with Pete Manolios on some ACL2 stuff, and we had a
> > > question regarding GCL. We are looking at building a Java frontend for
> > > ACL2, but the frequency and magnitude of interaction (e.g. browsing
> > > the logical universe) is such that a lightweight interface (i.e. no
> > > IPC) between Java and LISP would be ideal. It seems like this would be
> > > possible if GCL could compile an image to a shared object file instead
> > > of an executable. Then Java can load the .so file as a native library
> > > using the Java native interface. The trick would be getting the
> > > GCL-based LISP program to export symbols useful to Java. We wouldn't
> > > mind using a C wrapper to get some of this to happen.
> > >
> > > The main questions are: (1) does GCL have any support for this at
> > > present, or is there a clear way to accomplish this even if there is
> > > not explicit support? (2) are there any fundamental issues with LISP
> > > playing in an address space shared with Java? I could see Java
> > > disliking certain operations, like brk() and/or sbrk(), but I'm not
> > > even sure what Java approves/disapproves of in a native shared
> > > library.
> > >
> > > Any info would be appreciated.
> > >
> > > --
> > > Peter Dillinger | "Back off! I'm a scientist."
> > > address@hidden |
> > > http://www.peterd.org | - Dr. Peter Venkman
> > >
> > >
> > >
> > - --
> > Camm Maguire address@hidden
> > ==========================================================================
> > "The earth is but one country, and mankind its citizens." -- Baha'u'llah
> > ------- End of forwarded message -------
> Peter Dillinger | "Back off! I'm a scientist."
> address@hidden |
> http://www.peterd.org | - Dr. Peter Venkman
Camm Maguire address@hidden
"The earth is but one country, and mankind its citizens." -- Baha'u'llah
|[Prev in Thread]
||[Next in Thread]|
- [Gcl-devel] Re: ACL2 in Java,
Camm Maguire <=