[mercury-users] C Interface (was Circular lists)
Thomas Charles CONWAY
conway at cs.mu.oz.au
Fri Nov 28 07:58:56 AEDT 1997
Richard A. O'Keefe, you write:
> The Quintus interface, with *NO* access to Prolog data structures or control
> from C, was entirely adequate to do I/O, networking, IPC, &c. I believe a
> lower level access *to C structures* was provided to Prolog about the time
> I left. Peter Schachte can comment on this, because he implemented it.
> But Prolog access to C data structures is not the same as C access to
> Prolog data structures.
The Mercury interface to C does not provide access to Mercury
data structures. Any C code that manipulates Mercury data structures
does so relying on knowledge of the current implementation, and
is considered unsafe. It would be nice if we could detect if
the C code does manipulate Mercury data structures, but I think
that this is not something that we can without too many false
hits, or too many false misses.
> What I'm getting at is really incredibly simple: a subset of the interface
> that can be used to pass some subset of *C* data structures between Mercury
> and C, where an amazingly simple tool can say "yes, you have used no
> interface features outside that subset".
> You can do _all_ of I/O, networking, IPC, and graphics with an interface
> subset like that.
Agreed. The Tcl/Tk and OpenGL interfaces don't manipulate Mercury
data structures. The only "dangerous" thing that happens (memory
management/GC issues aside) is that we store a closure in a global
variable and get it back later.
> You might be surprised at just how checkable (new) C code can be.
> Perhaps we have different ideas on what is checkable from such a tool,
> and how large that checkable set needs to be before it is useful.
> Exactly. The Mercury team seem to have jumped to the conclusion that I meant
> some kind of universal theorem prover that could just about write the programs
> for you, whereas I want something much more modest: a list of safe interface
> features and a tool that checks that only those features are used.
I guess once we had a C parser, we could check for dereferencing or
casting of Mercury terms, however even something like this would be
a large amount of work to produce. The trick is the "once we had a
Thomas Conway conway at cs.mu.oz.au
AD DEUM ET VINUM Every sword has two edges.
More information about the users