source: Deliverables/D2.2/8051/src/utilities/Fix.ml @ 486

Last change on this file since 486 was 486, checked in by ayache, 9 years ago

Deliverable D2.2

File size: 18.1 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
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
23module 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
31end
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
49module type PROPERTY = sig
50  type property
51  val bottom: property
52  val equal: property -> property -> bool
53  val is_maximal: property -> bool
54end
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
68module 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. *)
102end
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 = List.filter (fun edge -> not edge.destroyed) node.incoming in
181    node.incoming <- predecessors;
182    List.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    List.iter (fun edge ->
215      assert (not edge.destroyed);
216      edge.destroyed <- true;
217    ) node.outgoing;
218    node.outgoing <- []
219
220end
221
222(* -------------------------------------------------------------------------- *)
223
224(* The code is parametric in an implementation of maps over variables and in
225   an implementation of properties. *)
226
227module Make
228  (M : IMPERATIVE_MAPS)
229  (P : PROPERTY)
230= struct
231
232type variable =
233    M.key
234
235type property =
236    P.property
237
238type valuation =
239    variable -> property
240
241type rhs =
242    valuation -> property
243
244type 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
254type node =
255    data Graph.node
256
257and 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
273let 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
281let 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
295module 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! *)
307end 
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
323end
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
338let signal subject =
339  List.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
353let 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
362let 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
369let 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
396let 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
489and 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
507let inactive =
508  ref true
509
510let 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
526end
527in LFP.get
528
529end
Note: See TracBrowser for help on using the repository browser.