Stack-based implementation of compiling parallel moves

parallel.ml

(**
   Iterative version of algorithm presented in
   the "Tilting at Windmills in Coq" paper;

   https://xavierleroy.org/publi/parallel-move.pdf

   The algorithm is effectively a post-order traversal of the transfer relation,
   accounting for cyclic dependencies along the way.

   Suppose the transfer relation had no cycles, for example: X -> Y -> Z;
   (arising from parallel assignment: (Y, Z) := (X, Y)).

   This must be emitted in the order:

     Z := Y;
     Y := X;

   This amounts processing "dependent" transfer relations for a given relation
   before processing the relation itself. In graph theory terms, continually processing nodes
   in a transfer relation that have an out-degree of 0 (then removing them from the graph; a very
   similar idea to running Kahn's topological sort algorithm on the transpose graph of the transfer
   relation).

   If we begin processing X -> Y, we must look for relations of the form Y -> ..., as these relations'
   source is dependent on the destination of the current transfer relation. So, we process these first.
   This amounts to processing the transfer relations in post-order (solving dependent subproblems first).

   However, a cycle may occur during this processing, where we begin to process a relation that's already
   started being processed (in recursive post-order terms, we meet a sub-problem again in a lower call stack).

   To deal with this, if X <- Y is the cyclic dependency, we emit t := Y and perform
   the in-place substitution: (X <- Y)[Y := t]. This ensures that sub-problems can freely populate Y in
   the meantime - because the cyclic dependency will finalise after these sub-problems (due to the nature of
   the post-order traversal) and, when it finally gets emitted, will emit X := t.
 *)

type status = Unmoved | Moving | Moved
type stage = Start | Finalise

let src = [|"rsi";"rdi";"rax";"rsi";"rax"|]
let dst = [|"rdi";"rsi";"rdx";"rcx";"r8"|]
let len = Array.length src
let status = Array.make len Unmoved

(* process transfer chain dependent on transfer relation at index i *)
let move i =
  let st = Stack.create () in
  Stack.push (Start, i) st;
  while not (Stack.is_empty st) do
    let (stage, i) = Stack.pop st in
    if src.(i) <> dst.(i) then
      match stage with
      | Start ->
         (match status.(i) with
          | Unmoved ->
             status.(i) <- Moving;
             (* remember to finalise this relation after solving its sub-problems *)
             Stack.push (Finalise, i) st;
             (* push, in reverse order, every relation whose source depends on the current definition *)
             for j = len - 1 downto 0 do
               if src.(j) = dst.(i) then
                 Stack.push (Start, j) st
             done
          | Moving ->
             (* we appear to have a cyclic sub-problem,
              preserve its source in a temporary that it will use later *)
             Printf.printf "mov t, %s\n" src.(i);
             src.(i) <- "t"
          | Moved -> ())
      | Finalise ->
         (* i's sub-problems have all been processed, emit the move *)
         Printf.printf "mov %s, %s\n" dst.(i) src.(i);
         status.(i) <- Moved
  done

(* ensure relations without dependencies are processed at least once *)
let () =
  Array.iteri
    (fun i _ ->
      if status.(i) = Unmoved then move i) src