1 | (**************************************************************************) |
---|
2 | (* *) |
---|
3 | (* Fix *) |
---|
4 | (* *) |
---|
5 | (* Author: François Pottier, INRIA Paris-Rocquencourt *) |
---|
6 | (* Version: 20091201 *) |
---|
7 | (* *) |
---|
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). *) |
---|
11 | (* *) |
---|
12 | (**************************************************************************) |
---|
13 | |
---|
14 | module MyList = struct |
---|
15 | let rec rev_append l1 l2 = |
---|
16 | match l1 with |
---|
17 | [] -> l2 |
---|
18 | | a :: l -> rev_append l (a :: l2) |
---|
19 | |
---|
20 | let rev l = rev_append l [] |
---|
21 | |
---|
22 | let find_all p = |
---|
23 | let rec find accu = function |
---|
24 | | [] -> rev accu |
---|
25 | | x :: l -> if p x then find (x :: accu) l else find accu l in |
---|
26 | find [] |
---|
27 | |
---|
28 | let filter = find_all |
---|
29 | |
---|
30 | let rec map f = function |
---|
31 | [] -> [] |
---|
32 | | a::l -> let r = f a in r :: map f l |
---|
33 | |
---|
34 | let rec iter f = function |
---|
35 | [] -> () |
---|
36 | | a::l -> f a; iter f l |
---|
37 | end |
---|
38 | |
---|
39 | (* -------------------------------------------------------------------------- *) |
---|
40 | |
---|
41 | (* Maps. *) |
---|
42 | |
---|
43 | (* We require imperative maps, that is, maps that can be updated in place. |
---|
44 | An implementation of persistent maps, such as the one offered by ocaml's |
---|
45 | standard library, can easily be turned into an implementation of imperative |
---|
46 | maps, so this is a weak requirement. *) |
---|
47 | |
---|
48 | module type IMPERATIVE_MAPS = sig |
---|
49 | type key |
---|
50 | type 'data t |
---|
51 | val create: unit -> 'data t |
---|
52 | val clear: 'data t -> unit |
---|
53 | val add: key -> 'data -> 'data t -> unit |
---|
54 | val find: key -> 'data t -> 'data |
---|
55 | val iter: (key -> 'data -> unit) -> 'data t -> unit |
---|
56 | end |
---|
57 | |
---|
58 | (* -------------------------------------------------------------------------- *) |
---|
59 | |
---|
60 | (* Properties. *) |
---|
61 | |
---|
62 | (* Properties must form a partial order, equipped with a least element, and |
---|
63 | must satisfy the ascending chain condition: every monotone sequence |
---|
64 | eventually stabilizes. *) |
---|
65 | |
---|
66 | (* [is_maximal] determines whether a property [p] is maximal with respect to |
---|
67 | the partial order. Only a conservative check is required: in any event, it |
---|
68 | is permitted for [is_maximal p] to return [false]. If [is_maximal p] |
---|
69 | returns [true], then [p] must have no upper bound other than itself. In |
---|
70 | particular, if properties form a lattice, then [p] must be the top |
---|
71 | element. This feature, not described in the paper, enables a couple of |
---|
72 | minor optimizations. *) |
---|
73 | |
---|
74 | module type PROPERTY = sig |
---|
75 | type property |
---|
76 | val bottom: property |
---|
77 | val equal: property -> property -> bool |
---|
78 | val is_maximal: property -> bool |
---|
79 | end |
---|
80 | |
---|
81 | (* -------------------------------------------------------------------------- *) |
---|
82 | |
---|
83 | (* The dynamic dependency graph. *) |
---|
84 | |
---|
85 | (* An edge from [node1] to [node2] means that [node1] depends on [node2], or |
---|
86 | (equivalently) that [node1] observes [node2]. Then, an update of the |
---|
87 | current property at [node2] causes a signal to be sent to [node1]. A node |
---|
88 | can observe itself. *) |
---|
89 | |
---|
90 | (* This module could be placed in a separate file, but is included here in |
---|
91 | order to make [Fix] self-contained. *) |
---|
92 | |
---|
93 | module Graph : sig |
---|
94 | |
---|
95 | (* This module provides a data structure for maintaining and modifying |
---|
96 | a directed graph. Each node is allowed to carry a piece of client |
---|
97 | data. There are functions for creating a new node, looking up a |
---|
98 | node's data, looking up a node's predecessors, and setting or |
---|
99 | clearing a node's successors (all at once). *) |
---|
100 | type 'data node |
---|
101 | |
---|
102 | (* [create data] creates a new node, with no incident edges, with |
---|
103 | client information [data]. Time complexity: constant. *) |
---|
104 | val create: 'data -> 'data node |
---|
105 | |
---|
106 | (* [data node] returns the client information associated with |
---|
107 | the node [node]. Time complexity: constant. *) |
---|
108 | val data: 'data node -> 'data |
---|
109 | |
---|
110 | (* [predecessors node] returns a list of [node]'s predecessors. |
---|
111 | Amortized time complexity: linear in the length of the output |
---|
112 | list. *) |
---|
113 | val predecessors: 'data node -> 'data node list |
---|
114 | |
---|
115 | (* [set_successors src dsts] creates an edge from the node [src] to |
---|
116 | each of the nodes in the list [dsts]. Duplicate elements in the |
---|
117 | list [dsts] are removed, so that no duplicate edges are created. It |
---|
118 | is assumed that [src] initially has no successors. Time complexity: |
---|
119 | linear in the length of the input list. *) |
---|
120 | val set_successors: 'data node -> 'data node list -> unit |
---|
121 | |
---|
122 | (* [clear_successors node] removes all of [node]'s outgoing edges. |
---|
123 | Time complexity: linear in the number of edges that are removed. *) |
---|
124 | val clear_successors: 'data node -> unit |
---|
125 | |
---|
126 | (* That's it. *) |
---|
127 | end |
---|
128 | = struct |
---|
129 | |
---|
130 | (* Using doubly-linked adjacency lists, one could implement [predecessors] |
---|
131 | in worst-case linear time with respect to the length of the output list, |
---|
132 | [set_successors] in worst-case linear time with respect to the length of |
---|
133 | the input list, and [clear_successors] in worst-case linear time with |
---|
134 | respect to the number of edges that are removed. We use a simpler |
---|
135 | implementation, based on singly-linked adjacency lists, with deferred |
---|
136 | removal of edges. It achieves the same complexity bounds, except |
---|
137 | [predecessors] only offers an amortized complexity bound. This is good |
---|
138 | enough for our purposes, and, in practice, is more efficient by a |
---|
139 | constant factor. This simplification was suggested by Arthur |
---|
140 | Charguéraud. *) |
---|
141 | |
---|
142 | type 'data node = { |
---|
143 | |
---|
144 | (* The client information associated with this node. *) |
---|
145 | |
---|
146 | data: 'data; |
---|
147 | |
---|
148 | (* This node's incoming and outgoing edges. *) |
---|
149 | |
---|
150 | mutable outgoing: 'data edge list; |
---|
151 | mutable incoming: 'data edge list; |
---|
152 | |
---|
153 | (* A transient mark, always set to [false], except when checking |
---|
154 | against duplicate elements in a successor list. *) |
---|
155 | |
---|
156 | mutable marked: bool; |
---|
157 | |
---|
158 | } |
---|
159 | |
---|
160 | and 'data edge = { |
---|
161 | |
---|
162 | (* This edge's nodes. Edges are symmetric: source and destination |
---|
163 | are not distinguished. Thus, an edge appears both in the outgoing |
---|
164 | edge list of its source node and in the incoming edge list of its |
---|
165 | destination node. This allows edges to be easily marked as |
---|
166 | destroyed. *) |
---|
167 | |
---|
168 | node1: 'data node; |
---|
169 | node2: 'data node; |
---|
170 | |
---|
171 | (* Edges that are destroyed are marked as such, but are not |
---|
172 | immediately removed from the adjacency lists. *) |
---|
173 | |
---|
174 | mutable destroyed: bool; |
---|
175 | |
---|
176 | } |
---|
177 | |
---|
178 | let create (data : 'data) : 'data node = { |
---|
179 | data = data; |
---|
180 | outgoing = []; |
---|
181 | incoming = []; |
---|
182 | marked = false; |
---|
183 | } |
---|
184 | |
---|
185 | let data (node : 'data node) : 'data = |
---|
186 | node.data |
---|
187 | |
---|
188 | (* [follow src edge] returns the node that is connected to [src] |
---|
189 | by [edge]. Time complexity: constant. *) |
---|
190 | |
---|
191 | let follow src edge = |
---|
192 | if edge.node1 == src then |
---|
193 | edge.node2 |
---|
194 | else begin |
---|
195 | assert (edge.node2 == src); |
---|
196 | edge.node1 |
---|
197 | end |
---|
198 | |
---|
199 | (* The [predecessors] function removes edges that have been marked |
---|
200 | destroyed. The cost of removing these has already been paid for, |
---|
201 | so the amortized time complexity of [predecessors] is linear in |
---|
202 | the length of the output list. *) |
---|
203 | |
---|
204 | let predecessors (node : 'data node) : 'data node list = |
---|
205 | let predecessors = MyList.filter (fun edge -> not edge.destroyed) node.incoming in |
---|
206 | node.incoming <- predecessors; |
---|
207 | MyList.map (follow node) predecessors |
---|
208 | |
---|
209 | (* [link src dst] creates a new edge from [src] to [dst], together |
---|
210 | with its reverse edge. Time complexity: constant. *) |
---|
211 | |
---|
212 | let link (src : 'data node) (dst : 'data node) : unit = |
---|
213 | let edge = { |
---|
214 | node1 = src; |
---|
215 | node2 = dst; |
---|
216 | destroyed = false; |
---|
217 | } in |
---|
218 | src.outgoing <- edge :: src.outgoing; |
---|
219 | dst.incoming <- edge :: dst.incoming |
---|
220 | |
---|
221 | let set_successors (src : 'data node) (dsts : 'data node list) : unit = |
---|
222 | assert (src.outgoing = []); |
---|
223 | let rec loop = function |
---|
224 | | [] -> |
---|
225 | () |
---|
226 | | dst :: dsts -> |
---|
227 | if dst.marked then |
---|
228 | loop dsts (* skip duplicate elements *) |
---|
229 | else begin |
---|
230 | dst.marked <- true; |
---|
231 | link src dst; |
---|
232 | loop dsts; |
---|
233 | dst.marked <- false |
---|
234 | end |
---|
235 | in |
---|
236 | loop dsts |
---|
237 | |
---|
238 | let clear_successors (node : 'data node) : unit = |
---|
239 | MyList.iter (fun edge -> |
---|
240 | assert (not edge.destroyed); |
---|
241 | edge.destroyed <- true; |
---|
242 | ) node.outgoing; |
---|
243 | node.outgoing <- [] |
---|
244 | |
---|
245 | end |
---|
246 | |
---|
247 | (* -------------------------------------------------------------------------- *) |
---|
248 | |
---|
249 | (* The code is parametric in an implementation of maps over variables and in |
---|
250 | an implementation of properties. *) |
---|
251 | |
---|
252 | module Make |
---|
253 | (M : IMPERATIVE_MAPS) |
---|
254 | (P : PROPERTY) |
---|
255 | = struct |
---|
256 | |
---|
257 | type variable = |
---|
258 | M.key |
---|
259 | |
---|
260 | type property = |
---|
261 | P.property |
---|
262 | |
---|
263 | type valuation = |
---|
264 | variable -> property |
---|
265 | |
---|
266 | type rhs = |
---|
267 | valuation -> property |
---|
268 | |
---|
269 | type equations = |
---|
270 | variable -> rhs |
---|
271 | |
---|
272 | (* -------------------------------------------------------------------------- *) |
---|
273 | |
---|
274 | (* Data. *) |
---|
275 | |
---|
276 | (* Each node in the dependency graph carries information about a fixed |
---|
277 | variable [v]. *) |
---|
278 | |
---|
279 | type node = |
---|
280 | data Graph.node |
---|
281 | |
---|
282 | and data = { |
---|
283 | |
---|
284 | (* This is the result of the application of [rhs] to the variable [v]. It |
---|
285 | must be stored in order to guarantee that this application is performed |
---|
286 | at most once. *) |
---|
287 | rhs: rhs; |
---|
288 | |
---|
289 | (* This is the current property at [v]. It evolves monotonically with |
---|
290 | time. *) |
---|
291 | mutable property: property; |
---|
292 | |
---|
293 | (* That's it! *) |
---|
294 | } |
---|
295 | |
---|
296 | (* [property node] returns the current property at [node]. *) |
---|
297 | |
---|
298 | let property node = |
---|
299 | (Graph.data node).property |
---|
300 | |
---|
301 | (* -------------------------------------------------------------------------- *) |
---|
302 | |
---|
303 | (* Many definitions must be made within the body of the function [lfp]. |
---|
304 | For greater syntactic convenience, we place them in a local module. *) |
---|
305 | |
---|
306 | let lfp (eqs : equations) : valuation = |
---|
307 | let module LFP = struct |
---|
308 | |
---|
309 | (* -------------------------------------------------------------------------- *) |
---|
310 | |
---|
311 | (* The workset. *) |
---|
312 | |
---|
313 | (* When the algorithm is inactive, the workset is empty. *) |
---|
314 | |
---|
315 | (* Our workset is based on a Queue, but it could just as well be based on a |
---|
316 | Stack. A textual replacement is possible. It could also be based on a |
---|
317 | priority queue, provided a sensible way of assigning priorities could |
---|
318 | be found. *) |
---|
319 | |
---|
320 | module Workset : sig |
---|
321 | |
---|
322 | (* [insert node] inserts [node] into the workset. [node] must have no |
---|
323 | successors. *) |
---|
324 | val insert: node -> unit |
---|
325 | |
---|
326 | (* [repeat f] repeatedly applies [f] to a node extracted out of the |
---|
327 | workset, until the workset becomes empty. [f] is allowed to use |
---|
328 | [insert]. *) |
---|
329 | val repeat: (node -> unit) -> unit |
---|
330 | |
---|
331 | (* That's it! *) |
---|
332 | end |
---|
333 | = struct |
---|
334 | |
---|
335 | (* Initialize the workset. *) |
---|
336 | |
---|
337 | let workset = |
---|
338 | Queue.create() |
---|
339 | |
---|
340 | let insert node = |
---|
341 | Queue.push node workset |
---|
342 | |
---|
343 | let repeat f = |
---|
344 | while not (Queue.is_empty workset) do |
---|
345 | f (Queue.pop workset) |
---|
346 | done |
---|
347 | |
---|
348 | end |
---|
349 | |
---|
350 | (* -------------------------------------------------------------------------- *) |
---|
351 | |
---|
352 | (* Signals. *) |
---|
353 | |
---|
354 | (* A node in the workset has no successors. (It can have predecessors.) In |
---|
355 | other words, a predecessor (an observer) of some node is never in the |
---|
356 | workset. Furthermore, a node never appears twice in the workset. *) |
---|
357 | |
---|
358 | (* When a variable broadcasts a signal, all of its predecessors (observers) |
---|
359 | receive the signal. Any variable that receives the signal loses all of its |
---|
360 | successors (that is, it ceases to observe anything) and is inserted into |
---|
361 | the workset. This preserves the above invariant. *) |
---|
362 | |
---|
363 | let signal subject = |
---|
364 | MyList.iter (fun observer -> |
---|
365 | Graph.clear_successors observer; |
---|
366 | Workset.insert observer |
---|
367 | ) (Graph.predecessors subject) |
---|
368 | (* At this point, [subject] has no predecessors. This plays no role in |
---|
369 | the correctness proof, though. *) |
---|
370 | |
---|
371 | (* -------------------------------------------------------------------------- *) |
---|
372 | |
---|
373 | (* Tables. *) |
---|
374 | |
---|
375 | (* The permanent table maps variables that have reached a fixed point |
---|
376 | to properties. It persists forever. *) |
---|
377 | |
---|
378 | let permanent : property M.t = |
---|
379 | M.create() |
---|
380 | |
---|
381 | (* The transient table maps variables that have not yet reached a |
---|
382 | fixed point to nodes. (A node contains not only a property, but |
---|
383 | also a memoized right-hand side, and carries edges.) At the |
---|
384 | beginning of a run, it is empty. It fills up during a run. At the |
---|
385 | end of a run, it is copied into the permanent table and cleared. *) |
---|
386 | |
---|
387 | let transient : node M.t = |
---|
388 | M.create() |
---|
389 | |
---|
390 | (* [freeze()] copies the transient table into the permanent table, and |
---|
391 | empties the transient table. This allows all nodes to be reclaimed |
---|
392 | by the garbage collector. *) |
---|
393 | |
---|
394 | let freeze () = |
---|
395 | M.iter (fun v node -> |
---|
396 | M.add v (property node) permanent |
---|
397 | ) transient; |
---|
398 | M.clear transient |
---|
399 | |
---|
400 | (* -------------------------------------------------------------------------- *) |
---|
401 | |
---|
402 | (* Workset processing. *) |
---|
403 | |
---|
404 | |
---|
405 | (* [solve node] re-evaluates the right-hand side at [node]. If this leads to |
---|
406 | a change, then the current property is updated, and [node] emits a signal |
---|
407 | towards its observers. *) |
---|
408 | |
---|
409 | (* When [solve node] is invoked, [node] has no subjects. Indeed, when [solve] |
---|
410 | is invoked by [node_for], [node] is newly created; when [solve] is invoked by |
---|
411 | [Workset.repeat], [node] has just been extracted out of the workset, and a |
---|
412 | node in the workset has no subjects. *) |
---|
413 | |
---|
414 | (* [node] must not be in the workset. *) |
---|
415 | |
---|
416 | (* In short, when [solve node] is invoked, [node] is neither awake nor asleep. |
---|
417 | When [solve node] finishes, [node] is either awake or asleep again. (Chances |
---|
418 | are, it is asleep, unless it is its own observer; then, it is awakened by the |
---|
419 | final call to [signal node].) *) |
---|
420 | |
---|
421 | let rec solve (node : node) : unit = |
---|
422 | |
---|
423 | (* Retrieve the data record carried by this node. *) |
---|
424 | let data = Graph.data node in |
---|
425 | |
---|
426 | (* Prepare to compute an updated value at this node. This is done by |
---|
427 | invoking the client's right-hand side function. *) |
---|
428 | |
---|
429 | (* The flag [alive] is used to prevent the client from invoking [request] |
---|
430 | after this interaction phase is over. In theory, this dynamic check seems |
---|
431 | required in order to argue that [request] behaves like a pure function. |
---|
432 | In practice, this check is not very useful: only a bizarre client would |
---|
433 | store a [request] function and invoke it after it has become stale. *) |
---|
434 | let alive = ref true |
---|
435 | and subjects = ref [] in |
---|
436 | |
---|
437 | (* We supply the client with [request], a function that provides access to |
---|
438 | the current valuation, and dynamically records dependencies. This yields |
---|
439 | a set of dependencies that is correct by construction. *) |
---|
440 | let request (v : variable) : property = |
---|
441 | assert !alive; |
---|
442 | try |
---|
443 | M.find v permanent |
---|
444 | with Not_found -> |
---|
445 | let subject = node_for v in |
---|
446 | let p = property subject in |
---|
447 | if not (P.is_maximal p) then |
---|
448 | subjects := subject :: !subjects; |
---|
449 | p |
---|
450 | in |
---|
451 | |
---|
452 | (* Give control to the client. *) |
---|
453 | let new_property = data.rhs request in |
---|
454 | |
---|
455 | (* From now on, prevent any invocation of this instance of [request] |
---|
456 | the client. *) |
---|
457 | alive := false; |
---|
458 | |
---|
459 | (* At this point, [node] has no subjects, as noted above. Thus, the |
---|
460 | precondition of [set_successors] is met. We can install [data.subjects] |
---|
461 | as the new set of subjects for this node. *) |
---|
462 | |
---|
463 | (* If we have gathered no subjects in the list [data.subjects], then |
---|
464 | this node must have stabilized. If [new_property] is maximal, |
---|
465 | then this node must have stabilized. *) |
---|
466 | |
---|
467 | (* If this node has stabilized, then it need not observe any more, so the |
---|
468 | call to [set_successors] is skipped. In practice, this seems to be a |
---|
469 | minor optimization. In the particular case where every node stabilizes at |
---|
470 | the very first call to [rhs], this means that no edges are ever |
---|
471 | built. This particular case is unlikely, as it means that we are just |
---|
472 | doing memoization, not a true fixed point computation. *) |
---|
473 | |
---|
474 | (* One could go further and note that, if this node has stabilized, then it |
---|
475 | could immediately be taken out of the transient table and copied into the |
---|
476 | permanent table. This would have the beneficial effect of allowing the |
---|
477 | detection of further nodes that have stabilized. Furthermore, it would |
---|
478 | enforce the property that no node in the transient table has a maximal |
---|
479 | value, hence the call to [is_maximal] above would become useless. *) |
---|
480 | |
---|
481 | if not (!subjects = [] || P.is_maximal new_property) then |
---|
482 | Graph.set_successors node !subjects; |
---|
483 | |
---|
484 | (* If the updated value differs from the previous value, record |
---|
485 | the updated value and send a signal to all observers of [node]. *) |
---|
486 | if not (P.equal data.property new_property) then begin |
---|
487 | data.property <- new_property; |
---|
488 | signal node |
---|
489 | end |
---|
490 | (* Note that equality of the two values does not imply that this node has |
---|
491 | stabilized forever. *) |
---|
492 | |
---|
493 | (* -------------------------------------------------------------------------- *) |
---|
494 | |
---|
495 | (* [node_for v] returns the graph node associated with the variable [v]. It is |
---|
496 | assumed that [v] does not appear in the permanent table. If [v] appears in |
---|
497 | the transient table, the associated node is returned. Otherwise, [v] is a |
---|
498 | newly discovered variable: a new node is created on the fly, and the |
---|
499 | transient table is grown. The new node can either be inserted into the |
---|
500 | workset (it is then awake) or handled immediately via a recursive call to |
---|
501 | [solve] (it is then asleep, unless it observes itself). *) |
---|
502 | |
---|
503 | (* The recursive call to [solve node] can be replaced, if desired, by a call |
---|
504 | to [Workset.insert node]. Using a recursive call to [solve] permits eager |
---|
505 | top-down discovery of new nodes. This can save a constant factor, because |
---|
506 | it allows new nodes to move directly from [bottom] to a good first |
---|
507 | approximation, without sending any signals, since [node] has no observers |
---|
508 | when [solve node] is invoked. In fact, if the dependency graph is acyclic, |
---|
509 | the algorithm discovers nodes top-down, performs computation on the way |
---|
510 | back up, and runs without ever inserting a node into the workset! |
---|
511 | Unfortunately, this causes the stack to grow as deep as the longest path in |
---|
512 | the dependency graph, which can blow up the stack. *) |
---|
513 | |
---|
514 | and node_for (v : variable) : node = |
---|
515 | try |
---|
516 | M.find v transient |
---|
517 | with Not_found -> |
---|
518 | let node = Graph.create { rhs = eqs v; property = P.bottom } in |
---|
519 | (* Adding this node to the transient table prior to calling [solve] |
---|
520 | recursively is mandatory, otherwise [solve] might loop, creating |
---|
521 | an infinite number of nodes for the same variable. *) |
---|
522 | M.add v node transient; |
---|
523 | solve node; (* or: Workset.insert node *) |
---|
524 | node |
---|
525 | |
---|
526 | (* -------------------------------------------------------------------------- *) |
---|
527 | |
---|
528 | (* Invocations of [get] trigger the fixed point computation. *) |
---|
529 | |
---|
530 | (* The flag [inactive] prevents reentrant calls by the client. *) |
---|
531 | |
---|
532 | let inactive = |
---|
533 | ref true |
---|
534 | |
---|
535 | let get (v : variable) : property = |
---|
536 | try |
---|
537 | M.find v permanent |
---|
538 | with Not_found -> |
---|
539 | assert !inactive; |
---|
540 | inactive := false; |
---|
541 | let node = node_for v in |
---|
542 | Workset.repeat solve; |
---|
543 | freeze(); |
---|
544 | inactive := true; |
---|
545 | property node |
---|
546 | |
---|
547 | (* -------------------------------------------------------------------------- *) |
---|
548 | |
---|
549 | (* Close the local module [LFP]. *) |
---|
550 | |
---|
551 | end |
---|
552 | in LFP.get |
---|
553 | |
---|
554 | end |
---|