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 | (* -------------------------------------------------------------------------- *) |
---|
15 | |
---|
16 | (* Maps. *) |
---|
17 | |
---|
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. *) |
---|
22 | |
---|
23 | module type IMPERATIVE_MAPS = sig |
---|
24 | type key |
---|
25 | type 'data t |
---|
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 |
---|
31 | end |
---|
32 | |
---|
33 | (* -------------------------------------------------------------------------- *) |
---|
34 | |
---|
35 | (* Properties. *) |
---|
36 | |
---|
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. *) |
---|
40 | |
---|
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. *) |
---|
48 | |
---|
49 | module type PROPERTY = sig |
---|
50 | type property |
---|
51 | val bottom: property |
---|
52 | val equal: property -> property -> bool |
---|
53 | val is_maximal: property -> bool |
---|
54 | end |
---|
55 | |
---|
56 | (* -------------------------------------------------------------------------- *) |
---|
57 | |
---|
58 | (* The dynamic dependency graph. *) |
---|
59 | |
---|
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. *) |
---|
64 | |
---|
65 | (* This module could be placed in a separate file, but is included here in |
---|
66 | order to make [Fix] self-contained. *) |
---|
67 | |
---|
68 | module Graph : sig |
---|
69 | |
---|
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). *) |
---|
75 | type 'data node |
---|
76 | |
---|
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 |
---|
80 | |
---|
81 | (* [data node] returns the client information associated with |
---|
82 | the node [node]. Time complexity: constant. *) |
---|
83 | val data: 'data node -> 'data |
---|
84 | |
---|
85 | (* [predecessors node] returns a list of [node]'s predecessors. |
---|
86 | Amortized time complexity: linear in the length of the output |
---|
87 | list. *) |
---|
88 | val predecessors: 'data node -> 'data node list |
---|
89 | |
---|
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 |
---|
96 | |
---|
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 |
---|
100 | |
---|
101 | (* That's it. *) |
---|
102 | end |
---|
103 | = struct |
---|
104 | |
---|
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 |
---|
115 | Charguéraud. *) |
---|
116 | |
---|
117 | type 'data node = { |
---|
118 | |
---|
119 | (* The client information associated with this node. *) |
---|
120 | |
---|
121 | data: 'data; |
---|
122 | |
---|
123 | (* This node's incoming and outgoing edges. *) |
---|
124 | |
---|
125 | mutable outgoing: 'data edge list; |
---|
126 | mutable incoming: 'data edge list; |
---|
127 | |
---|
128 | (* A transient mark, always set to [false], except when checking |
---|
129 | against duplicate elements in a successor list. *) |
---|
130 | |
---|
131 | mutable marked: bool; |
---|
132 | |
---|
133 | } |
---|
134 | |
---|
135 | and 'data edge = { |
---|
136 | |
---|
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 |
---|
141 | destroyed. *) |
---|
142 | |
---|
143 | node1: 'data node; |
---|
144 | node2: 'data node; |
---|
145 | |
---|
146 | (* Edges that are destroyed are marked as such, but are not |
---|
147 | immediately removed from the adjacency lists. *) |
---|
148 | |
---|
149 | mutable destroyed: bool; |
---|
150 | |
---|
151 | } |
---|
152 | |
---|
153 | let create (data : 'data) : 'data node = { |
---|
154 | data = data; |
---|
155 | outgoing = []; |
---|
156 | incoming = []; |
---|
157 | marked = false; |
---|
158 | } |
---|
159 | |
---|
160 | let data (node : 'data node) : 'data = |
---|
161 | node.data |
---|
162 | |
---|
163 | (* [follow src edge] returns the node that is connected to [src] |
---|
164 | by [edge]. Time complexity: constant. *) |
---|
165 | |
---|
166 | let follow src edge = |
---|
167 | if edge.node1 == src then |
---|
168 | edge.node2 |
---|
169 | else begin |
---|
170 | assert (edge.node2 == src); |
---|
171 | edge.node1 |
---|
172 | end |
---|
173 | |
---|
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. *) |
---|
178 | |
---|
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 |
---|
183 | |
---|
184 | (* [link src dst] creates a new edge from [src] to [dst], together |
---|
185 | with its reverse edge. Time complexity: constant. *) |
---|
186 | |
---|
187 | let link (src : 'data node) (dst : 'data node) : unit = |
---|
188 | let edge = { |
---|
189 | node1 = src; |
---|
190 | node2 = dst; |
---|
191 | destroyed = false; |
---|
192 | } in |
---|
193 | src.outgoing <- edge :: src.outgoing; |
---|
194 | dst.incoming <- edge :: dst.incoming |
---|
195 | |
---|
196 | let set_successors (src : 'data node) (dsts : 'data node list) : unit = |
---|
197 | assert (src.outgoing = []); |
---|
198 | let rec loop = function |
---|
199 | | [] -> |
---|
200 | () |
---|
201 | | dst :: dsts -> |
---|
202 | if dst.marked then |
---|
203 | loop dsts (* skip duplicate elements *) |
---|
204 | else begin |
---|
205 | dst.marked <- true; |
---|
206 | link src dst; |
---|
207 | loop dsts; |
---|
208 | dst.marked <- false |
---|
209 | end |
---|
210 | in |
---|
211 | loop dsts |
---|
212 | |
---|
213 | let clear_successors (node : 'data node) : unit = |
---|
214 | OcamlList.iter (fun edge -> |
---|
215 | assert (not edge.destroyed); |
---|
216 | edge.destroyed <- true; |
---|
217 | ) node.outgoing; |
---|
218 | node.outgoing <- [] |
---|
219 | |
---|
220 | end |
---|
221 | |
---|
222 | (* -------------------------------------------------------------------------- *) |
---|
223 | |
---|
224 | (* The code is parametric in an implementation of maps over variables and in |
---|
225 | an implementation of properties. *) |
---|
226 | |
---|
227 | module Make |
---|
228 | (M : IMPERATIVE_MAPS) |
---|
229 | (P : PROPERTY) |
---|
230 | = struct |
---|
231 | |
---|
232 | type variable = |
---|
233 | M.key |
---|
234 | |
---|
235 | type property = |
---|
236 | P.property |
---|
237 | |
---|
238 | type valuation = |
---|
239 | variable -> property |
---|
240 | |
---|
241 | type rhs = |
---|
242 | valuation -> property |
---|
243 | |
---|
244 | type equations = |
---|
245 | variable -> rhs |
---|
246 | |
---|
247 | (* -------------------------------------------------------------------------- *) |
---|
248 | |
---|
249 | (* Data. *) |
---|
250 | |
---|
251 | (* Each node in the dependency graph carries information about a fixed |
---|
252 | variable [v]. *) |
---|
253 | |
---|
254 | type node = |
---|
255 | data Graph.node |
---|
256 | |
---|
257 | and data = { |
---|
258 | |
---|
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 |
---|
261 | at most once. *) |
---|
262 | rhs: rhs; |
---|
263 | |
---|
264 | (* This is the current property at [v]. It evolves monotonically with |
---|
265 | time. *) |
---|
266 | mutable property: property; |
---|
267 | |
---|
268 | (* That's it! *) |
---|
269 | } |
---|
270 | |
---|
271 | (* [property node] returns the current property at [node]. *) |
---|
272 | |
---|
273 | let property node = |
---|
274 | (Graph.data node).property |
---|
275 | |
---|
276 | (* -------------------------------------------------------------------------- *) |
---|
277 | |
---|
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. *) |
---|
280 | |
---|
281 | let lfp (eqs : equations) : valuation = |
---|
282 | let module LFP = struct |
---|
283 | |
---|
284 | (* -------------------------------------------------------------------------- *) |
---|
285 | |
---|
286 | (* The workset. *) |
---|
287 | |
---|
288 | (* When the algorithm is inactive, the workset is empty. *) |
---|
289 | |
---|
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 |
---|
293 | be found. *) |
---|
294 | |
---|
295 | module Workset : sig |
---|
296 | |
---|
297 | (* [insert node] inserts [node] into the workset. [node] must have no |
---|
298 | successors. *) |
---|
299 | val insert: node -> unit |
---|
300 | |
---|
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 |
---|
303 | [insert]. *) |
---|
304 | val repeat: (node -> unit) -> unit |
---|
305 | |
---|
306 | (* That's it! *) |
---|
307 | end |
---|
308 | = struct |
---|
309 | |
---|
310 | (* Initialize the workset. *) |
---|
311 | |
---|
312 | let workset = |
---|
313 | Queue.create() |
---|
314 | |
---|
315 | let insert node = |
---|
316 | Queue.push node workset |
---|
317 | |
---|
318 | let repeat f = |
---|
319 | while not (Queue.is_empty workset) do |
---|
320 | f (Queue.pop workset) |
---|
321 | done |
---|
322 | |
---|
323 | end |
---|
324 | |
---|
325 | (* -------------------------------------------------------------------------- *) |
---|
326 | |
---|
327 | (* Signals. *) |
---|
328 | |
---|
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. *) |
---|
332 | |
---|
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. *) |
---|
337 | |
---|
338 | let signal subject = |
---|
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. *) |
---|
345 | |
---|
346 | (* -------------------------------------------------------------------------- *) |
---|
347 | |
---|
348 | (* Tables. *) |
---|
349 | |
---|
350 | (* The permanent table maps variables that have reached a fixed point |
---|
351 | to properties. It persists forever. *) |
---|
352 | |
---|
353 | let permanent : property M.t = |
---|
354 | M.create() |
---|
355 | |
---|
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. *) |
---|
361 | |
---|
362 | let transient : node M.t = |
---|
363 | M.create() |
---|
364 | |
---|
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. *) |
---|
368 | |
---|
369 | let freeze () = |
---|
370 | M.iter (fun v node -> |
---|
371 | M.add v (property node) permanent |
---|
372 | ) transient; |
---|
373 | M.clear transient |
---|
374 | |
---|
375 | (* -------------------------------------------------------------------------- *) |
---|
376 | |
---|
377 | (* Workset processing. *) |
---|
378 | |
---|
379 | |
---|
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. *) |
---|
383 | |
---|
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. *) |
---|
388 | |
---|
389 | (* [node] must not be in the workset. *) |
---|
390 | |
---|
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].) *) |
---|
395 | |
---|
396 | let rec solve (node : node) : unit = |
---|
397 | |
---|
398 | (* Retrieve the data record carried by this node. *) |
---|
399 | let data = Graph.data node in |
---|
400 | |
---|
401 | (* Prepare to compute an updated value at this node. This is done by |
---|
402 | invoking the client's right-hand side function. *) |
---|
403 | |
---|
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. *) |
---|
409 | let alive = ref true |
---|
410 | and subjects = ref [] in |
---|
411 | |
---|
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 = |
---|
416 | assert !alive; |
---|
417 | try |
---|
418 | M.find v permanent |
---|
419 | with Not_found -> |
---|
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; |
---|
424 | p |
---|
425 | in |
---|
426 | |
---|
427 | (* Give control to the client. *) |
---|
428 | let new_property = data.rhs request in |
---|
429 | |
---|
430 | (* From now on, prevent any invocation of this instance of [request] |
---|
431 | the client. *) |
---|
432 | alive := false; |
---|
433 | |
---|
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. *) |
---|
437 | |
---|
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. *) |
---|
441 | |
---|
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. *) |
---|
448 | |
---|
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. *) |
---|
455 | |
---|
456 | if not (!subjects = [] || P.is_maximal new_property) then |
---|
457 | Graph.set_successors node !subjects; |
---|
458 | |
---|
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; |
---|
463 | signal node |
---|
464 | end |
---|
465 | (* Note that equality of the two values does not imply that this node has |
---|
466 | stabilized forever. *) |
---|
467 | |
---|
468 | (* -------------------------------------------------------------------------- *) |
---|
469 | |
---|
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). *) |
---|
477 | |
---|
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. *) |
---|
488 | |
---|
489 | and node_for (v : variable) : node = |
---|
490 | try |
---|
491 | M.find v transient |
---|
492 | with Not_found -> |
---|
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 *) |
---|
499 | node |
---|
500 | |
---|
501 | (* -------------------------------------------------------------------------- *) |
---|
502 | |
---|
503 | (* Invocations of [get] trigger the fixed point computation. *) |
---|
504 | |
---|
505 | (* The flag [inactive] prevents reentrant calls by the client. *) |
---|
506 | |
---|
507 | let inactive = |
---|
508 | ref true |
---|
509 | |
---|
510 | let get (v : variable) : property = |
---|
511 | try |
---|
512 | M.find v permanent |
---|
513 | with Not_found -> |
---|
514 | assert !inactive; |
---|
515 | inactive := false; |
---|
516 | let node = node_for v in |
---|
517 | Workset.repeat solve; |
---|
518 | freeze(); |
---|
519 | inactive := true; |
---|
520 | property node |
---|
521 | |
---|
522 | (* -------------------------------------------------------------------------- *) |
---|
523 | |
---|
524 | (* Close the local module [LFP]. *) |
---|
525 | |
---|
526 | end |
---|
527 | in LFP.get |
---|
528 | |
---|
529 | end |
---|