source: extracted/Fix.ml @ 2736

Last change on this file since 2736 was 2736, checked in by sacerdot, 6 years ago

Untrusted fixpoint computation branched in.

File size: 18.6 KB
Line 
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
14module MyList = struct
15let rec rev_append l1 l2 =
16  match l1 with
17    [] -> l2
18  | a :: l -> rev_append l (a :: l2)
19
20let rev l = rev_append l []
21
22let 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
28let filter = find_all
29
30let rec map f = function
31    [] -> []
32  | a::l -> let r = f a in r :: map f l
33
34let rec iter f = function
35    [] -> ()
36  | a::l -> f a; iter f l
37end
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
48module 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
56end
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
74module type PROPERTY = sig
75  type property
76  val bottom: property
77  val equal: property -> property -> bool
78  val is_maximal: property -> bool
79end
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
93module 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. *)
127end
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
245end
246
247(* -------------------------------------------------------------------------- *)
248
249(* The code is parametric in an implementation of maps over variables and in
250   an implementation of properties. *)
251
252module Make
253  (M : IMPERATIVE_MAPS)
254  (P : PROPERTY)
255= struct
256
257type variable =
258    M.key
259
260type property =
261    P.property
262
263type valuation =
264    variable -> property
265
266type rhs =
267    valuation -> property
268
269type 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
279type node =
280    data Graph.node
281
282and 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
298let 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
306let 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
320module 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! *)
332end 
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
348end
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
363let 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
378let 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
387let 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
394let 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
421let 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
514and 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
532let inactive =
533  ref true
534
535let 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
551end
552in LFP.get
553
554end
Note: See TracBrowser for help on using the repository browser.