•Keep two pieces of state for each procedure F:
–CF is current thread in F
–SF is first thread after next sync statement
in F.
•In both orders, insert new threads after current thread
•On spawn, insert continuation thread before spawn thread in one order. Do the opposite in the other.
•On sync, advance CF to SF
•In any other thread, update shadow spaces based on current thread