RE: [Caml-list] recursive modules redux, & interface files

["Manuel Fahndrich" <maf@microsoft.com>]

To add more fuel to this interesting conversation, I've recently come
across a nice analogy between recursive modules and the assume-guarantee
rules known from model checking. The assume-guarantee rule in model
checking allows models to be checked relatively independently. In
general, the AG rule takes on the form

	AI | B <= BI
	A | BI <= AI
    ------------------- [some side conditions]
	A | B <= AI | BI

where A and B are two processes, and we want to check that the parallel
composition A | B conforms to some interface AI | BI. In general, it is
not the case that A <= AI and B <= BI, which would lead to the result.
Instead, some amount of information about the interactions between A and
B are needed. This is expressed in the preconditions AI | B <= BI, i.e.,
we check that B composed with the interface specification of A (AI)
conforms to BI, and similarly for A. 

The side conditions depend on the particular domain being modeled. If
the models are synchronous and asynchronous logic circuits, then the
side conditions express that there cannot be any logical circularities
between module A and B, ie. mutually recursive definitions of wires that
do not involve at least one latch.

Now what does this have to do with recursive modules? May be by now this
is obvious, but let me say it anyway. In the context of recursive
modules, composition is linking, and conformance is interface checking.
If we have two modules A and B that are mutually recursive and we want
to ascribe interfaces AI and BI to these, it may be the case that we
cannot do that independently, that is we can only ascribe these
interfaces, given that we know we will link A with something conforming
to BI and link B with something conforming to AI, ie., we can use the
assume guarantee rule.
The notation AI | B <= BI then simply states that in order to verify
that B has interface BI, we also need to know the interfaces AI of
module A that will be linked with B.

What about the side conditions? It turns out that the side conditions of
an assume guarantee rule for modules is very similar to that of logical
circuits, namely, we cannot have any circular definitions of values that
do not involve a function abstraction (a delay).

	module A = struct let (x:int) = B.y end
      module B = struct let (y:int) = A.x end

contains such a circular definition, whereas 

	module A = struct let fx () = B.fy () end
      module B = struct let fy () = A.fx () end

Thus the side conditions are concerned with correct initialization. This
is of course not new, Crary and Harper have given sufficient conditions
on recursive module definitions for these properties to be true, and I
suppose Claudio Russo has similar conditions, although I haven't read
his thesis yet.

Regards,

-Manuel Fahndrich
 

-----Original Message-----
From: Xavier Leroy [mailto:Xavier.Leroy@inria.fr] 
Sent: Tuesday, March 27, 2001 1:01 AM
To: Don Syme
Cc: caml-list@inria.fr
Subject: Re: [Caml-list] recursive modules redux, & interface files

> Isn't it feasible to annotate elements of signatures with something
that
> indicates that an identifier really is bound to a value, rather than a
> module??  i.e.

You probably meant "rather than a result of an arbitrary computation".
Yes, it can be done this way, and I believe such annotations in
signatures are necessary for a full treatment of recursion between
modules (the Holy Grail :-).  However, they also pollute signatures
with "implementation details".

For more modest forms of recursion, e.g. cross-recursion between
compilation units, I was hoping this information could be propagated
behind the scene, without cluttering signatures, or just re-inferred and
checked at link-time.  This is just a vague idea.

Cheers,

- Xavier Leroy
-------------------
To unsubscribe, mail caml-list-request@inria.fr.  Archives:
http://caml.inria.fr
-------------------
To unsubscribe, mail caml-list-request@inria.fr.  Archives: http://caml.inria.fr