Imported Upstream version 0.1

[pkg-cerco/acc-trusted.git] / extracted / untrusted / Fix.ml

(**************************************************************************)
(*                                                                        *)
(*  Fix                                                                   *)
(*                                                                        *)
(*  Author:  François Pottier, INRIA Paris-Rocquencourt                   *)
(*  Version: 20091201                                                     *)
(*                                                                        *)
(*  The copyright to this code is held by Institut National de Recherche  *)
(*  en Informatique et en Automatique (INRIA). All rights reserved. This  *)
(*  file is distributed under the license CeCILL-C (see file LICENSE).    *)
(*                                                                        *)
(**************************************************************************)

(* -------------------------------------------------------------------------- *)

(* Maps. *)

(* We require imperative maps, that is, maps that can be updated in place.
   An implementation of persistent maps, such as the one offered by ocaml's
   standard library, can easily be turned into an implementation of imperative
   maps, so this is a weak requirement. *)

module type IMPERATIVE_MAPS = sig
  type key
  type 'data t
  val create: unit -> 'data t
  val clear: 'data t -> unit
  val add: key -> 'data -> 'data t -> unit
  val find: key -> 'data t -> 'data
  val iter: (key -> 'data -> unit) -> 'data t -> unit
end

(* -------------------------------------------------------------------------- *)

(* Properties. *)

(* Properties must form a partial order, equipped with a least element, and
   must satisfy the ascending chain condition: every monotone sequence
   eventually stabilizes. *)

(* [is_maximal] determines whether a property [p] is maximal with respect to
   the partial order. Only a conservative check is required: in any event, it
   is permitted for [is_maximal p] to return [false]. If [is_maximal p]
   returns [true], then [p] must have no upper bound other than itself. In
   particular, if properties form a lattice, then [p] must be the top
   element. This feature, not described in the paper, enables a couple of
   minor optimizations. *)

module type PROPERTY = sig
  type property
  val bottom: property
  val equal: property -> property -> bool
  val is_maximal: property -> bool
end

(* -------------------------------------------------------------------------- *)

(* The dynamic dependency graph. *)

(* An edge from [node1] to [node2] means that [node1] depends on [node2], or
   (equivalently) that [node1] observes [node2]. Then, an update of the
   current property at [node2] causes a signal to be sent to [node1]. A node
   can observe itself. *)

(* This module could be placed in a separate file, but is included here in
   order to make [Fix] self-contained. *)

module Graph : sig

  (* This module provides a data structure for maintaining and modifying
     a directed graph. Each node is allowed to carry a piece of client
     data. There are functions for creating a new node, looking up a
     node's data, looking up a node's predecessors, and setting or
     clearing a node's successors (all at once). *)
  type 'data node

  (* [create data] creates a new node, with no incident edges, with
     client information [data]. Time complexity: constant. *)
  val create: 'data -> 'data node

  (* [data node] returns the client information associated with
     the node [node]. Time complexity: constant. *)
  val data: 'data node -> 'data

  (* [predecessors node] returns a list of [node]'s predecessors.
     Amortized time complexity: linear in the length of the output
     list. *)
  val predecessors: 'data node -> 'data node list

  (* [set_successors src dsts] creates an edge from the node [src] to
     each of the nodes in the list [dsts]. Duplicate elements in the
     list [dsts] are removed, so that no duplicate edges are created. It
     is assumed that [src] initially has no successors. Time complexity:
     linear in the length of the input list. *)
  val set_successors: 'data node -> 'data node list -> unit

  (* [clear_successors node] removes all of [node]'s outgoing edges.
     Time complexity: linear in the number of edges that are removed. *)
  val clear_successors: 'data node -> unit

  (* That's it. *)
end
= struct

  (* Using doubly-linked adjacency lists, one could implement [predecessors]
     in worst-case linear time with respect to the length of the output list,
     [set_successors] in worst-case linear time with respect to the length of
     the input list, and [clear_successors] in worst-case linear time with
     respect to the number of edges that are removed. We use a simpler
     implementation, based on singly-linked adjacency lists, with deferred
     removal of edges. It achieves the same complexity bounds, except
     [predecessors] only offers an amortized complexity bound. This is good
     enough for our purposes, and, in practice, is more efficient by a
     constant factor. This simplification was suggested by Arthur
     Charguéraud. *)

  type 'data node = {

    (* The client information associated with this node. *)

    data: 'data;

    (* This node's incoming and outgoing edges. *)

    mutable outgoing: 'data edge list;
    mutable incoming: 'data edge list;

    (* A transient mark, always set to [false], except when checking
       against duplicate elements in a successor list. *)

    mutable marked: bool;

  }

  and 'data edge = {

    (* This edge's nodes. Edges are symmetric: source and destination
       are not distinguished. Thus, an edge appears both in the outgoing
       edge list of its source node and in the incoming edge list of its
       destination node. This allows edges to be easily marked as
       destroyed. *)

    node1: 'data node;
    node2: 'data node;

    (* Edges that are destroyed are marked as such, but are not
       immediately removed from the adjacency lists. *)

    mutable destroyed: bool;

  }

  let create (data : 'data) : 'data node = {
    data = data;
    outgoing = [];
    incoming = [];
    marked = false;
  }

  let data (node : 'data node) : 'data =
    node.data

  (* [follow src edge] returns the node that is connected to [src]
     by [edge]. Time complexity: constant. *)

  let follow src edge =
    if edge.node1 == src then
      edge.node2
    else begin
      assert (edge.node2 == src);
      edge.node1
    end

  (* The [predecessors] function removes edges that have been marked
     destroyed. The cost of removing these has already been paid for,
     so the amortized time complexity of [predecessors] is linear in
     the length of the output list. *)

  let predecessors (node : 'data node) : 'data node list =
    let predecessors = OcamlList.filter (fun edge -> not edge.destroyed) node.incoming in
    node.incoming <- predecessors;
    OcamlList.map (follow node) predecessors

  (* [link src dst] creates a new edge from [src] to [dst], together
     with its reverse edge. Time complexity: constant. *)

  let link (src : 'data node) (dst : 'data node) : unit =
    let edge = {
      node1 = src;
      node2 = dst;
      destroyed = false;
    } in
    src.outgoing <- edge :: src.outgoing;
    dst.incoming <- edge :: dst.incoming

  let set_successors (src : 'data node) (dsts : 'data node list) : unit =
    assert (src.outgoing = []);
    let rec loop = function
      | [] ->
          ()
      | dst :: dsts ->
          if dst.marked then
            loop dsts (* skip duplicate elements *)
          else begin
            dst.marked <- true;
            link src dst;
            loop dsts;
            dst.marked <- false
          end
    in
    loop dsts

  let clear_successors (node : 'data node) : unit =
    OcamlList.iter (fun edge ->
      assert (not edge.destroyed);
      edge.destroyed <- true;
    ) node.outgoing;
    node.outgoing <- []

end

(* -------------------------------------------------------------------------- *)

(* The code is parametric in an implementation of maps over variables and in
   an implementation of properties. *)

module Make
  (M : IMPERATIVE_MAPS)
  (P : PROPERTY)
= struct

type variable =
    M.key

type property =
    P.property

type valuation =
    variable -> property

type rhs =
    valuation -> property

type equations =
    variable -> rhs

(* -------------------------------------------------------------------------- *)

(* Data. *)

(* Each node in the dependency graph carries information about a fixed
   variable [v]. *)

type node =
    data Graph.node

and data = {

  (* This is the result of the application of [rhs] to the variable [v]. It
     must be stored in order to guarantee that this application is performed
     at most once. *)
  rhs: rhs;

  (* This is the current property at [v]. It evolves monotonically with
     time. *)
  mutable property: property;

  (* That's it! *)
}

(* [property node] returns the current property at [node]. *)

let property node =
  (Graph.data node).property

(* -------------------------------------------------------------------------- *)

(* Many definitions must be made within the body of the function [lfp].
   For greater syntactic convenience, we place them in a local module. *)

let lfp (eqs : equations) : valuation =
  let module LFP = struct

(* -------------------------------------------------------------------------- *)

(* The workset. *)

(* When the algorithm is inactive, the workset is empty. *)

(* Our workset is based on a Queue, but it could just as well be based on a
   Stack. A textual replacement is possible. It could also be based on a
   priority queue, provided a sensible way of assigning priorities could
   be found. *)

module Workset : sig

  (* [insert node] inserts [node] into the workset. [node] must have no
     successors. *)
  val insert: node -> unit  

  (* [repeat f] repeatedly applies [f] to a node extracted out of the
     workset, until the workset becomes empty. [f] is allowed to use
     [insert]. *)
  val repeat: (node -> unit) -> unit

  (* That's it! *)
end 
= struct

  (* Initialize the workset. *)

  let workset =
    Queue.create()

  let insert node =
    Queue.push node workset

  let repeat f =
    while not (Queue.is_empty workset) do
      f (Queue.pop workset)
    done

end

(* -------------------------------------------------------------------------- *)

(* Signals. *)

(* A node in the workset has no successors. (It can have predecessors.)  In
   other words, a predecessor (an observer) of some node is never in the
   workset. Furthermore, a node never appears twice in the workset. *)

(* When a variable broadcasts a signal, all of its predecessors (observers)
   receive the signal. Any variable that receives the signal loses all of its
   successors (that is, it ceases to observe anything) and is inserted into
   the workset. This preserves the above invariant. *)

let signal subject =
  OcamlList.iter (fun observer ->
    Graph.clear_successors observer;
    Workset.insert observer
  ) (Graph.predecessors subject)
  (* At this point, [subject] has no predecessors. This plays no role in
     the correctness proof, though. *)

(* -------------------------------------------------------------------------- *)

(* Tables. *)

(* The permanent table maps variables that have reached a fixed point
   to properties. It persists forever. *)

let permanent : property M.t =
  M.create()

(* The transient table maps variables that have not yet reached a
   fixed point to nodes. (A node contains not only a property, but
   also a memoized right-hand side, and carries edges.) At the
   beginning of a run, it is empty. It fills up during a run. At the
   end of a run, it is copied into the permanent table and cleared. *)

let transient : node M.t =
  M.create()

(* [freeze()] copies the transient table into the permanent table, and
   empties the transient table. This allows all nodes to be reclaimed
   by the garbage collector. *)

let freeze () =
  M.iter (fun v node ->
    M.add v (property node) permanent
  ) transient;
  M.clear transient

(* -------------------------------------------------------------------------- *)

(* Workset processing. *)


(* [solve node] re-evaluates the right-hand side at [node]. If this leads to
   a change, then the current property is updated, and [node] emits a signal
   towards its observers. *)

(* When [solve node] is invoked, [node] has no subjects. Indeed, when [solve]
   is invoked by [node_for], [node] is newly created; when [solve] is invoked by
   [Workset.repeat], [node] has just been extracted out of the workset, and a
   node in the workset has no subjects. *)

(* [node] must not be in the workset. *)

(* In short, when [solve node] is invoked, [node] is neither awake nor asleep.
   When [solve node] finishes, [node] is either awake or asleep again. (Chances
   are, it is asleep, unless it is its own observer; then, it is awakened by the
   final call to [signal node].) *)

let rec solve (node : node) : unit =

  (* Retrieve the data record carried by this node. *)
  let data = Graph.data node in

  (* Prepare to compute an updated value at this node. This is done by
     invoking the client's right-hand side function.  *)

  (* The flag [alive] is used to prevent the client from invoking [request]
     after this interaction phase is over. In theory, this dynamic check seems
     required in order to argue that [request] behaves like a pure function.
     In practice, this check is not very useful: only a bizarre client would
     store a [request] function and invoke it after it has become stale. *)
  let alive = ref true
  and subjects = ref [] in

  (* We supply the client with [request], a function that provides access to
     the current valuation, and dynamically records dependencies. This yields
     a set of dependencies that is correct by construction. *)
  let request (v : variable) : property =
    assert !alive;
    try
      M.find v permanent
    with Not_found ->
      let subject = node_for v in
      let p = property subject in
      if not (P.is_maximal p) then
        subjects := subject :: !subjects;
      p
  in

  (* Give control to the client. *)
  let new_property = data.rhs request in

  (* From now on, prevent any invocation of this instance of [request]
     the client. *)
  alive := false;

  (* At this point, [node] has no subjects, as noted above. Thus, the
     precondition of [set_successors] is met. We can install [data.subjects]
     as the new set of subjects for this node. *)

  (* If we have gathered no subjects in the list [data.subjects], then
     this node must have stabilized. If [new_property] is maximal,
     then this node must have stabilized. *)

  (* If this node has stabilized, then it need not observe any more, so the
     call to [set_successors] is skipped. In practice, this seems to be a
     minor optimization. In the particular case where every node stabilizes at
     the very first call to [rhs], this means that no edges are ever
     built. This particular case is unlikely, as it means that we are just
     doing memoization, not a true fixed point computation. *)

  (* One could go further and note that, if this node has stabilized, then it
     could immediately be taken out of the transient table and copied into the
     permanent table. This would have the beneficial effect of allowing the
     detection of further nodes that have stabilized. Furthermore, it would
     enforce the property that no node in the transient table has a maximal
     value, hence the call to [is_maximal] above would become useless. *)

  if not (!subjects = [] || P.is_maximal new_property) then
    Graph.set_successors node !subjects;

  (* If the updated value differs from the previous value, record
     the updated value and send a signal to all observers of [node]. *)
  if not (P.equal data.property new_property) then begin
    data.property <- new_property;
    signal node
  end
  (* Note that equality of the two values does not imply that this node has
     stabilized forever. *)

(* -------------------------------------------------------------------------- *)

(* [node_for v] returns the graph node associated with the variable [v]. It is
   assumed that [v] does not appear in the permanent table. If [v] appears in
   the transient table, the associated node is returned. Otherwise, [v] is a
   newly discovered variable: a new node is created on the fly, and the
   transient table is grown. The new node can either be inserted into the
   workset (it is then awake) or handled immediately via a recursive call to
   [solve] (it is then asleep, unless it observes itself). *)

(* The recursive call to [solve node] can be replaced, if desired, by a call
   to [Workset.insert node]. Using a recursive call to [solve] permits eager
   top-down discovery of new nodes. This can save a constant factor, because
   it allows new nodes to move directly from [bottom] to a good first
   approximation, without sending any signals, since [node] has no observers
   when [solve node] is invoked. In fact, if the dependency graph is acyclic,
   the algorithm discovers nodes top-down, performs computation on the way
   back up, and runs without ever inserting a node into the workset!
   Unfortunately, this causes the stack to grow as deep as the longest path in
   the dependency graph, which can blow up the stack. *)

and node_for (v : variable) : node =
  try
    M.find v transient
  with Not_found ->
    let node = Graph.create { rhs = eqs v; property = P.bottom } in
    (* Adding this node to the transient table prior to calling [solve]
       recursively is mandatory, otherwise [solve] might loop, creating
       an infinite number of nodes for the same variable. *)
    M.add v node transient;
    solve node; (* or: Workset.insert node *)
    node

(* -------------------------------------------------------------------------- *)

(* Invocations of [get] trigger the fixed point computation. *)

(* The flag [inactive] prevents reentrant calls by the client. *)

let inactive =
  ref true

let get (v : variable) : property =
  try
    M.find v permanent
  with Not_found ->
    assert !inactive;
    inactive := false;
    let node = node_for v in
    Workset.repeat solve;
    freeze();
    inactive := true;
    property node

(* -------------------------------------------------------------------------- *)

(* Close the local module [LFP]. *)

end
in LFP.get

end