Skip to content

Instantly share code, notes, and snippets.

Last active June 21, 2023 00:53
Show Gist options
  • Save contificate/87377cd9f451891b58d5b9b24906720b to your computer and use it in GitHub Desktop.
Save contificate/87377cd9f451891b58d5b9b24906720b to your computer and use it in GitHub Desktop.
Stack-based implementation of compiling parallel moves
Iterative version of algorithm presented in
the "Tilting at Windmills in Coq" paper;
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
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
| 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
(* ensure relations without dependencies are processed at least once *)
let () =
(fun i _ ->
if status.(i) = Unmoved then move i) src
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment