7de3c542ecca36af3e8f6306f0b271e8b9a90aa8
1 (**************************************************************************)
5 (* François Pottier, INRIA Rocquencourt *)
6 (* Yann Régis-Gianas, PPS, Université Paris Diderot *)
8 (* Copyright 2005-2008 Institut National de Recherche en Informatique *)
9 (* et en Automatique. All rights reserved. This file is distributed *)
10 (* under the terms of the Q Public License version 1.0, with the change *)
11 (* described in file LICENSE. *)
13 (**************************************************************************)
15 (* -------------------------------------------------------------------------- *)
19 (* We require imperative maps, that is, maps that can be updated in place.
20 An implementation of persistent maps, such as the one offered by ocaml's
21 standard library, can easily be turned into an implementation of imperative
22 maps, so this is a weak requirement. *)
24 module type IMPERATIVE_MAPS
= sig
27 val create
: unit -> 'data t
28 val clear
: 'data t
-> unit
29 val add
: key
-> 'data
-> 'data t
-> unit
30 val find
: key
-> 'data t
-> 'data
31 val iter
: (key
-> 'data
-> unit) -> 'data t
-> unit
34 (* -------------------------------------------------------------------------- *)
38 (* Properties must form a partial order, equipped with a least element, and
39 must satisfy the ascending chain condition: every monotone sequence
40 eventually stabilizes. *)
42 (* [is_maximal] determines whether a property [p] is maximal with respect to
43 the partial order. Only a conservative check is required: in any event, it
44 is permitted for [is_maximal p] to return [false]. If [is_maximal p]
45 returns [true], then [p] must have no upper bound other than itself. In
46 particular, if properties form a lattice, then [p] must be the top
47 element. This feature, not described in the paper, enables a couple of
48 minor optimizations. *)
50 module type PROPERTY
= sig
53 val equal
: property
-> property
-> bool
54 val is_maximal
: property
-> bool
57 (* -------------------------------------------------------------------------- *)
59 (* The dynamic dependency graph. *)
61 (* An edge from [node1] to [node2] means that [node1] depends on [node2], or
62 (equivalently) that [node1] observes [node2]. Then, an update of the
63 current property at [node2] causes a signal to be sent to [node1]. A node
64 can observe itself. *)
66 (* This module could be placed in a separate file, but is included here in
67 order to make [Fix] self-contained. *)
71 (* This module provides a data structure for maintaining and modifying
72 a directed graph. Each node is allowed to carry a piece of client
73 data. There are functions for creating a new node, looking up a
74 node's data, looking up a node's predecessors, and setting or
75 clearing a node's successors (all at once). *)
78 (* [create data] creates a new node, with no incident edges, with
79 client information [data]. Time complexity: constant. *)
80 val create
: 'data
-> 'data node
82 (* [data node] returns the client information associated with
83 the node [node]. Time complexity: constant. *)
84 val data
: 'data node
-> 'data
86 (* [predecessors node] returns a list of [node]'s predecessors.
87 Amortized time complexity: linear in the length of the output
89 val predecessors
: 'data node
-> 'data node list
91 (* [set_successors src dsts] creates an edge from the node [src] to
92 each of the nodes in the list [dsts]. Duplicate elements in the
93 list [dsts] are removed, so that no duplicate edges are created. It
94 is assumed that [src] initially has no successors. Time complexity:
95 linear in the length of the input list. *)
96 val set_successors
: 'data node
-> 'data node list
-> unit
98 (* [clear_successors node] removes all of [node]'s outgoing edges.
99 Time complexity: linear in the number of edges that are removed. *)
100 val clear_successors
: 'data node
-> unit
106 (* Using doubly-linked adjacency lists, one could implement [predecessors]
107 in worst-case linear time with respect to the length of the output list,
108 [set_successors] in worst-case linear time with respect to the length of
109 the input list, and [clear_successors] in worst-case linear time with
110 respect to the number of edges that are removed. We use a simpler
111 implementation, based on singly-linked adjacency lists, with deferred
112 removal of edges. It achieves the same complexity bounds, except
113 [predecessors] only offers an amortized complexity bound. This is good
114 enough for our purposes, and, in practice, is more efficient by a
115 constant factor. This simplification was suggested by Arthur
120 (* The client information associated with this node. *)
124 (* This node's incoming and outgoing edges. *)
126 mutable outgoing
: 'data edge list
;
127 mutable incoming
: 'data edge list
;
129 (* A transient mark, always set to [false], except when checking
130 against duplicate elements in a successor list. *)
132 mutable marked
: bool;
138 (* This edge's nodes. Edges are symmetric: source and destination
139 are not distinguished. Thus, an edge appears both in the outgoing
140 edge list of its source node and in the incoming edge list of its
141 destination node. This allows edges to be easily marked as
147 (* Edges that are destroyed are marked as such, but are not
148 immediately removed from the adjacency lists. *)
150 mutable destroyed
: bool;
154 let create (data
: 'data
) : 'data node
= {
161 let data (node
: '
data node
) : '
data =
164 (* [follow src edge] returns the node that is connected to [src]
165 by [edge]. Time complexity: constant. *)
167 let follow src edge
=
168 if edge
.node1
== src
then
171 assert (edge
.node2
== src
);
175 (* The [predecessors] function removes edges that have been marked
176 destroyed. The cost of removing these has already been paid for,
177 so the amortized time complexity of [predecessors] is linear in
178 the length of the output list. *)
180 let predecessors (node
: '
data node
) : '
data node list
=
181 let predecessors = List.filter
(fun edge
-> not edge
.destroyed
) node
.incoming
in
182 node
.incoming
<- predecessors;
183 List.map
(follow node
) predecessors
185 (* [link src dst] creates a new edge from [src] to [dst], together
186 with its reverse edge. Time complexity: constant. *)
188 let link (src
: '
data node
) (dst
: '
data node
) : unit =
194 src
.outgoing
<- edge :: src
.outgoing
;
195 dst
.incoming
<- edge :: dst
.incoming
197 let set_successors (src
: '
data node
) (dsts
: '
data node list
) : unit =
198 assert (src
.outgoing
= []);
199 let rec loop = function
204 loop dsts
(* skip duplicate elements *)
214 let clear_successors (node
: '
data node
) : unit =
215 List.iter
(fun edge ->
216 assert (not
edge.destroyed
);
217 edge.destroyed
<- true;
223 (* -------------------------------------------------------------------------- *)
225 (* The code is parametric in an implementation of maps over variables and in
226 an implementation of properties. *)
229 (M
: IMPERATIVE_MAPS
)
243 valuation
-> property
248 (* -------------------------------------------------------------------------- *)
252 (* Each node in the dependency graph carries information about a fixed
260 (* This is the result of the application of [rhs] to the variable [v]. It
261 must be stored in order to guarantee that this application is performed
265 (* This is the current property at [v]. It evolves monotonically with
267 mutable property
: property
;
272 (* [property node] returns the current property at [node]. *)
275 (Graph.data node
).property
277 (* -------------------------------------------------------------------------- *)
279 (* Many definitions must be made within the body of the function [lfp].
280 For greater syntactic convenience, we place them in a local module. *)
282 let lfp (eqs
: equations
) : valuation
=
283 let module LFP
= struct
285 (* -------------------------------------------------------------------------- *)
289 (* When the algorithm is inactive, the workset is empty. *)
291 (* Our workset is based on a Queue, but it could just as well be based on a
292 Stack. A textual replacement is possible. It could also be based on a
293 priority queue, provided a sensible way of assigning priorities could
298 (* [insert node] inserts [node] into the workset. [node] must have no
300 val insert
: node
-> unit
302 (* [repeat f] repeatedly applies [f] to a node extracted out of the
303 workset, until the workset becomes empty. [f] is allowed to use
305 val repeat
: (node
-> unit) -> unit
311 (* Initialize the workset. *)
317 Queue.push node
workset
320 while not
(Queue.is_empty
workset) do
321 f
(Queue.pop
workset)
326 (* -------------------------------------------------------------------------- *)
330 (* A node in the workset has no successors. (It can have predecessors.) In
331 other words, a predecessor (an observer) of some node is never in the
332 workset. Furthermore, a node never appears twice in the workset. *)
334 (* When a variable broadcasts a signal, all of its predecessors (observers)
335 receive the signal. Any variable that receives the signal loses all of its
336 successors (that is, it ceases to observe anything) and is inserted into
337 the workset. This preserves the above invariant. *)
340 List.iter
(fun observer
->
341 Graph.clear_successors observer
;
342 Workset.insert observer
343 ) (Graph.predecessors subject
)
344 (* At this point, [subject] has no predecessors. This plays no role in
345 the correctness proof, though. *)
347 (* -------------------------------------------------------------------------- *)
351 (* The permanent table maps variables that have reached a fixed point
352 to properties. It persists forever. *)
354 let permanent : property M.t
=
357 (* The transient table maps variables that have not yet reached a
358 fixed point to nodes. (A node contains not only a property, but
359 also a memoized right-hand side, and carries edges.) At the
360 beginning of a run, it is empty. It fills up during a run. At the
361 end of a run, it is copied into the permanent table and cleared. *)
363 let transient : node
M.t
=
366 (* [freeze()] copies the transient table into the permanent table, and
367 empties the transient table. This allows all nodes to be reclaimed
368 by the garbage collector. *)
371 M.iter
(fun v node
->
372 M.add v
(property node
) permanent
376 (* -------------------------------------------------------------------------- *)
378 (* Workset processing. *)
381 (* [solve node] re-evaluates the right-hand side at [node]. If this leads to
382 a change, then the current property is updated, and [node] emits a signal
383 towards its observers. *)
385 (* When [solve node] is invoked, [node] has no subjects. Indeed, when [solve]
386 is invoked by [node_for], [node] is newly created; when [solve] is invoked by
387 [Workset.repeat], [node] has just been extracted out of the workset, and a
388 node in the workset has no subjects. *)
390 (* [node] must not be in the workset. *)
392 (* In short, when [solve node] is invoked, [node] is neither awake nor asleep.
393 When [solve node] finishes, [node] is either awake or asleep again. (Chances
394 are, it is asleep, unless it is its own observer; then, it is awakened by the
395 final call to [signal node].) *)
397 let rec solve (node
: node
) : unit =
399 (* Retrieve the data record carried by this node. *)
400 let data = Graph.data node
in
402 (* Prepare to compute an updated value at this node. This is done by
403 invoking the client's right-hand side function. *)
405 (* The flag [alive] is used to prevent the client from invoking [request]
406 after this interaction phase is over. In theory, this dynamic check seems
407 required in order to argue that [request] behaves like a pure function.
408 In practice, this check is not very useful: only a bizarre client would
409 store a [request] function and invoke it after it has become stale. *)
411 and subjects
= ref [] in
413 (* We supply the client with [request], a function that provides access to
414 the current valuation, and dynamically records dependencies. This yields
415 a set of dependencies that is correct by construction. *)
416 let request (v
: variable
) : property =
421 let subject = node_for v
in
422 let p = property subject in
423 if not
(P.is_maximal
p) then
424 subjects
:= subject :: !subjects
;
428 (* Give control to the client. *)
429 let new_property = data.rhs
request in
431 (* From now on, prevent any invocation of this instance of [request]
435 (* At this point, [node] has no subjects, as noted above. Thus, the
436 precondition of [set_successors] is met. We can install [data.subjects]
437 as the new set of subjects for this node. *)
439 (* If we have gathered no subjects in the list [data.subjects], then
440 this node must have stabilized. If [new_property] is maximal,
441 then this node must have stabilized. *)
443 (* If this node has stabilized, then it need not observe any more, so the
444 call to [set_successors] is skipped. In practice, this seems to be a
445 minor optimization. In the particular case where every node stabilizes at
446 the very first call to [rhs], this means that no edges are ever
447 built. This particular case is unlikely, as it means that we are just
448 doing memoization, not a true fixed point computation. *)
450 (* One could go further and note that, if this node has stabilized, then it
451 could immediately be taken out of the transient table and copied into the
452 permanent table. This would have the beneficial effect of allowing the
453 detection of further nodes that have stabilized. Furthermore, it would
454 enforce the property that no node in the transient table has a maximal
455 value, hence the call to [is_maximal] above would become useless. *)
457 if not
(!subjects
= [] || P.is_maximal
new_property) then
458 Graph.set_successors node
!subjects
;
460 (* If the updated value differs from the previous value, record
461 the updated value and send a signal to all observers of [node]. *)
462 if not
(P.equal
data.property new_property) then begin
463 data.property <- new_property;
466 (* Note that equality of the two values does not imply that this node has
467 stabilized forever. *)
469 (* -------------------------------------------------------------------------- *)
471 (* [node_for v] returns the graph node associated with the variable [v]. It is
472 assumed that [v] does not appear in the permanent table. If [v] appears in
473 the transient table, the associated node is returned. Otherwise, [v] is a
474 newly discovered variable: a new node is created on the fly, and the
475 transient table is grown. The new node can either be inserted into the
476 workset (it is then awake) or handled immediately via a recursive call to
477 [solve] (it is then asleep, unless it observes itself). *)
479 (* The recursive call to [solve node] can be replaced, if desired, by a call
480 to [Workset.insert node]. Using a recursive call to [solve] permits eager
481 top-down discovery of new nodes. This can save a constant factor, because
482 it allows new nodes to move directly from [bottom] to a good first
483 approximation, without sending any signals, since [node] has no observers
484 when [solve node] is invoked. In fact, if the dependency graph is acyclic,
485 the algorithm discovers nodes top-down, performs computation on the way
486 back up, and runs without ever inserting a node into the workset!
487 Unfortunately, this causes the stack to grow as deep as the longest path in
488 the dependency graph, which can blow up the stack. *)
490 and node_for
(v
: variable
) : node
=
494 let node = Graph.create { rhs
= eqs v
; property = P.bottom
} in
495 (* Adding this node to the transient table prior to calling [solve]
496 recursively is mandatory, otherwise [solve] might loop, creating
497 an infinite number of nodes for the same variable. *)
498 M.add v
node transient;
499 solve node; (* or: Workset.insert node *)
502 (* -------------------------------------------------------------------------- *)
504 (* Invocations of [get] trigger the fixed point computation. *)
506 (* The flag [inactive] prevents reentrant calls by the client. *)
511 let get (v
: variable
) : property =
517 let node = node_for v
in
518 Workset.repeat solve;
523 (* -------------------------------------------------------------------------- *)
525 (* Close the local module [LFP]. *)