Synchronization And Entailment

• Synchronization is more than just simple dataflow
• Based on the notion of entailment

Consider:

case E of g(a) then {Show yes} else {Show no} end

This will block until it can be proven or disproven that E matches g(a), i.e. until the equation E=g(a) is entailed or disentailed.

• entailed = is a logical consequence of current constraints
• disentailed = the negation is ...

• when E=b: disentailed
• when E=g(X): blocks until X=a is entailed or disentailed
• when E=g(a): entailed