1 (**************************************************************************)
5 (* Author: François Pottier, INRIA Paris-Rocquencourt *)
6 (* Version: 20091201 *)
8 (* The copyright to this code is held by Institut National de Recherche *)
9 (* en Informatique et en Automatique (INRIA). All rights reserved. This *)
10 (* file is distributed under the license CeCILL-C (see file LICENSE). *)
12 (**************************************************************************)
14 (* -------------------------------------------------------------------------- *)
18 (* We require imperative maps, that is, maps that can be updated in place.
19 An implementation of persistent maps, such as the one offered by ocaml's
20 standard library, can easily be turned into an implementation of imperative
21 maps, so this is a weak requirement. *)
23 module type IMPERATIVE_MAPS = sig
26 val create: unit -> 'data t
27 val clear: 'data t -> unit
28 val add: key -> 'data -> 'data t -> unit
29 val find: key -> 'data t -> 'data
30 val iter: (key -> 'data -> unit) -> 'data t -> unit
33 (* -------------------------------------------------------------------------- *)
37 (* Properties must form a partial order, equipped with a least element, and
38 must satisfy the ascending chain condition: every monotone sequence
39 eventually stabilizes. *)
41 (* [is_maximal] determines whether a property [p] is maximal with respect to
42 the partial order. Only a conservative check is required: in any event, it
43 is permitted for [is_maximal p] to return [false]. If [is_maximal p]
44 returns [true], then [p] must have no upper bound other than itself. In
45 particular, if properties form a lattice, then [p] must be the top
46 element. This feature, not described in the paper, enables a couple of
47 minor optimizations. *)
49 module type PROPERTY = sig
52 val equal: property -> property -> bool
53 val is_maximal: property -> bool
56 (* -------------------------------------------------------------------------- *)
58 (* The dynamic dependency graph. *)
60 (* An edge from [node1] to [node2] means that [node1] depends on [node2], or
61 (equivalently) that [node1] observes [node2]. Then, an update of the
62 current property at [node2] causes a signal to be sent to [node1]. A node
63 can observe itself. *)
65 (* This module could be placed in a separate file, but is included here in
66 order to make [Fix] self-contained. *)
70 (* This module provides a data structure for maintaining and modifying
71 a directed graph. Each node is allowed to carry a piece of client
72 data. There are functions for creating a new node, looking up a
73 node's data, looking up a node's predecessors, and setting or
74 clearing a node's successors (all at once). *)
77 (* [create data] creates a new node, with no incident edges, with
78 client information [data]. Time complexity: constant. *)
79 val create: 'data -> 'data node
81 (* [data node] returns the client information associated with
82 the node [node]. Time complexity: constant. *)
83 val data: 'data node -> 'data
85 (* [predecessors node] returns a list of [node]'s predecessors.
86 Amortized time complexity: linear in the length of the output
88 val predecessors: 'data node -> 'data node list
90 (* [set_successors src dsts] creates an edge from the node [src] to
91 each of the nodes in the list [dsts]. Duplicate elements in the
92 list [dsts] are removed, so that no duplicate edges are created. It
93 is assumed that [src] initially has no successors. Time complexity:
94 linear in the length of the input list. *)
95 val set_successors: 'data node -> 'data node list -> unit
97 (* [clear_successors node] removes all of [node]'s outgoing edges.
98 Time complexity: linear in the number of edges that are removed. *)
99 val clear_successors: 'data node -> unit
105 (* Using doubly-linked adjacency lists, one could implement [predecessors]
106 in worst-case linear time with respect to the length of the output list,
107 [set_successors] in worst-case linear time with respect to the length of
108 the input list, and [clear_successors] in worst-case linear time with
109 respect to the number of edges that are removed. We use a simpler
110 implementation, based on singly-linked adjacency lists, with deferred
111 removal of edges. It achieves the same complexity bounds, except
112 [predecessors] only offers an amortized complexity bound. This is good
113 enough for our purposes, and, in practice, is more efficient by a
114 constant factor. This simplification was suggested by Arthur
119 (* The client information associated with this node. *)
123 (* This node's incoming and outgoing edges. *)
125 mutable outgoing: 'data edge list;
126 mutable incoming: 'data edge list;
128 (* A transient mark, always set to [false], except when checking
129 against duplicate elements in a successor list. *)
131 mutable marked: bool;
137 (* This edge's nodes. Edges are symmetric: source and destination
138 are not distinguished. Thus, an edge appears both in the outgoing
139 edge list of its source node and in the incoming edge list of its
140 destination node. This allows edges to be easily marked as
146 (* Edges that are destroyed are marked as such, but are not
147 immediately removed from the adjacency lists. *)
149 mutable destroyed: bool;
153 let create (data : 'data) : 'data node = {
160 let data (node : 'data node) : 'data =
163 (* [follow src edge] returns the node that is connected to [src]
164 by [edge]. Time complexity: constant. *)
166 let follow src edge =
167 if edge.node1 == src then
170 assert (edge.node2 == src);
174 (* The [predecessors] function removes edges that have been marked
175 destroyed. The cost of removing these has already been paid for,
176 so the amortized time complexity of [predecessors] is linear in
177 the length of the output list. *)
179 let predecessors (node : 'data node) : 'data node list =
180 let predecessors = OcamlList.filter (fun edge -> not edge.destroyed) node.incoming in
181 node.incoming <- predecessors;
182 OcamlList.map (follow node) predecessors
184 (* [link src dst] creates a new edge from [src] to [dst], together
185 with its reverse edge. Time complexity: constant. *)
187 let link (src : 'data node) (dst : 'data node) : unit =
193 src.outgoing <- edge :: src.outgoing;
194 dst.incoming <- edge :: dst.incoming
196 let set_successors (src : 'data node) (dsts : 'data node list) : unit =
197 assert (src.outgoing = []);
198 let rec loop = function
203 loop dsts (* skip duplicate elements *)
213 let clear_successors (node : 'data node) : unit =
214 OcamlList.iter (fun edge ->
215 assert (not edge.destroyed);
216 edge.destroyed <- true;
222 (* -------------------------------------------------------------------------- *)
224 (* The code is parametric in an implementation of maps over variables and in
225 an implementation of properties. *)
228 (M : IMPERATIVE_MAPS)
242 valuation -> property
247 (* -------------------------------------------------------------------------- *)
251 (* Each node in the dependency graph carries information about a fixed
259 (* This is the result of the application of [rhs] to the variable [v]. It
260 must be stored in order to guarantee that this application is performed
264 (* This is the current property at [v]. It evolves monotonically with
266 mutable property: property;
271 (* [property node] returns the current property at [node]. *)
274 (Graph.data node).property
276 (* -------------------------------------------------------------------------- *)
278 (* Many definitions must be made within the body of the function [lfp].
279 For greater syntactic convenience, we place them in a local module. *)
281 let lfp (eqs : equations) : valuation =
282 let module LFP = struct
284 (* -------------------------------------------------------------------------- *)
288 (* When the algorithm is inactive, the workset is empty. *)
290 (* Our workset is based on a Queue, but it could just as well be based on a
291 Stack. A textual replacement is possible. It could also be based on a
292 priority queue, provided a sensible way of assigning priorities could
297 (* [insert node] inserts [node] into the workset. [node] must have no
299 val insert: node -> unit
301 (* [repeat f] repeatedly applies [f] to a node extracted out of the
302 workset, until the workset becomes empty. [f] is allowed to use
304 val repeat: (node -> unit) -> unit
310 (* Initialize the workset. *)
316 Queue.push node workset
319 while not (Queue.is_empty workset) do
320 f (Queue.pop workset)
325 (* -------------------------------------------------------------------------- *)
329 (* A node in the workset has no successors. (It can have predecessors.) In
330 other words, a predecessor (an observer) of some node is never in the
331 workset. Furthermore, a node never appears twice in the workset. *)
333 (* When a variable broadcasts a signal, all of its predecessors (observers)
334 receive the signal. Any variable that receives the signal loses all of its
335 successors (that is, it ceases to observe anything) and is inserted into
336 the workset. This preserves the above invariant. *)
339 OcamlList.iter (fun observer ->
340 Graph.clear_successors observer;
341 Workset.insert observer
342 ) (Graph.predecessors subject)
343 (* At this point, [subject] has no predecessors. This plays no role in
344 the correctness proof, though. *)
346 (* -------------------------------------------------------------------------- *)
350 (* The permanent table maps variables that have reached a fixed point
351 to properties. It persists forever. *)
353 let permanent : property M.t =
356 (* The transient table maps variables that have not yet reached a
357 fixed point to nodes. (A node contains not only a property, but
358 also a memoized right-hand side, and carries edges.) At the
359 beginning of a run, it is empty. It fills up during a run. At the
360 end of a run, it is copied into the permanent table and cleared. *)
362 let transient : node M.t =
365 (* [freeze()] copies the transient table into the permanent table, and
366 empties the transient table. This allows all nodes to be reclaimed
367 by the garbage collector. *)
370 M.iter (fun v node ->
371 M.add v (property node) permanent
375 (* -------------------------------------------------------------------------- *)
377 (* Workset processing. *)
380 (* [solve node] re-evaluates the right-hand side at [node]. If this leads to
381 a change, then the current property is updated, and [node] emits a signal
382 towards its observers. *)
384 (* When [solve node] is invoked, [node] has no subjects. Indeed, when [solve]
385 is invoked by [node_for], [node] is newly created; when [solve] is invoked by
386 [Workset.repeat], [node] has just been extracted out of the workset, and a
387 node in the workset has no subjects. *)
389 (* [node] must not be in the workset. *)
391 (* In short, when [solve node] is invoked, [node] is neither awake nor asleep.
392 When [solve node] finishes, [node] is either awake or asleep again. (Chances
393 are, it is asleep, unless it is its own observer; then, it is awakened by the
394 final call to [signal node].) *)
396 let rec solve (node : node) : unit =
398 (* Retrieve the data record carried by this node. *)
399 let data = Graph.data node in
401 (* Prepare to compute an updated value at this node. This is done by
402 invoking the client's right-hand side function. *)
404 (* The flag [alive] is used to prevent the client from invoking [request]
405 after this interaction phase is over. In theory, this dynamic check seems
406 required in order to argue that [request] behaves like a pure function.
407 In practice, this check is not very useful: only a bizarre client would
408 store a [request] function and invoke it after it has become stale. *)
410 and subjects = ref [] in
412 (* We supply the client with [request], a function that provides access to
413 the current valuation, and dynamically records dependencies. This yields
414 a set of dependencies that is correct by construction. *)
415 let request (v : variable) : property =
420 let subject = node_for v in
421 let p = property subject in
422 if not (P.is_maximal p) then
423 subjects := subject :: !subjects;
427 (* Give control to the client. *)
428 let new_property = data.rhs request in
430 (* From now on, prevent any invocation of this instance of [request]
434 (* At this point, [node] has no subjects, as noted above. Thus, the
435 precondition of [set_successors] is met. We can install [data.subjects]
436 as the new set of subjects for this node. *)
438 (* If we have gathered no subjects in the list [data.subjects], then
439 this node must have stabilized. If [new_property] is maximal,
440 then this node must have stabilized. *)
442 (* If this node has stabilized, then it need not observe any more, so the
443 call to [set_successors] is skipped. In practice, this seems to be a
444 minor optimization. In the particular case where every node stabilizes at
445 the very first call to [rhs], this means that no edges are ever
446 built. This particular case is unlikely, as it means that we are just
447 doing memoization, not a true fixed point computation. *)
449 (* One could go further and note that, if this node has stabilized, then it
450 could immediately be taken out of the transient table and copied into the
451 permanent table. This would have the beneficial effect of allowing the
452 detection of further nodes that have stabilized. Furthermore, it would
453 enforce the property that no node in the transient table has a maximal
454 value, hence the call to [is_maximal] above would become useless. *)
456 if not (!subjects = [] || P.is_maximal new_property) then
457 Graph.set_successors node !subjects;
459 (* If the updated value differs from the previous value, record
460 the updated value and send a signal to all observers of [node]. *)
461 if not (P.equal data.property new_property) then begin
462 data.property <- new_property;
465 (* Note that equality of the two values does not imply that this node has
466 stabilized forever. *)
468 (* -------------------------------------------------------------------------- *)
470 (* [node_for v] returns the graph node associated with the variable [v]. It is
471 assumed that [v] does not appear in the permanent table. If [v] appears in
472 the transient table, the associated node is returned. Otherwise, [v] is a
473 newly discovered variable: a new node is created on the fly, and the
474 transient table is grown. The new node can either be inserted into the
475 workset (it is then awake) or handled immediately via a recursive call to
476 [solve] (it is then asleep, unless it observes itself). *)
478 (* The recursive call to [solve node] can be replaced, if desired, by a call
479 to [Workset.insert node]. Using a recursive call to [solve] permits eager
480 top-down discovery of new nodes. This can save a constant factor, because
481 it allows new nodes to move directly from [bottom] to a good first
482 approximation, without sending any signals, since [node] has no observers
483 when [solve node] is invoked. In fact, if the dependency graph is acyclic,
484 the algorithm discovers nodes top-down, performs computation on the way
485 back up, and runs without ever inserting a node into the workset!
486 Unfortunately, this causes the stack to grow as deep as the longest path in
487 the dependency graph, which can blow up the stack. *)
489 and node_for (v : variable) : node =
493 let node = Graph.create { rhs = eqs v; property = P.bottom } in
494 (* Adding this node to the transient table prior to calling [solve]
495 recursively is mandatory, otherwise [solve] might loop, creating
496 an infinite number of nodes for the same variable. *)
497 M.add v node transient;
498 solve node; (* or: Workset.insert node *)
501 (* -------------------------------------------------------------------------- *)
503 (* Invocations of [get] trigger the fixed point computation. *)
505 (* The flag [inactive] prevents reentrant calls by the client. *)
510 let get (v : variable) : property =
516 let node = node_for v in
517 Workset.repeat solve;
522 (* -------------------------------------------------------------------------- *)
524 (* Close the local module [LFP]. *)