Skip to content

WIP: Support sequential languages.

David Swasey requested to merge swasey/sequential into master

Sequential WP based on concurrent WP:

SWP e @ E1,E2 {{ Φ }} := |={E1,∅}=> WP e @ ∅ {{ v, |={∅,E2}=> Φ v }}

This definition is well-typed thanks to a canonical structure implementing a concurrent language (that does not fork) given a sequential language.

The nifty thing about this approach is proof sharing: The core structural rules, lifting lemmas, and adequacy for SWP use lemmas about WP, making proofs shorter than they'd be under a direct definition of SWP. (The ownP compatibility layer is basically a copy of the original. Ugly!)

The sequential language interface assumes a relation on machine configurations. @janno suggests taking sequential languages as primitive and defining the threadpool simulation and WP on top of the sequential language interface and SWP. The point would be to make the "base" language interface more widely applicable.

This is very much a work in progress: I have not added support for ectx languages or triples, and I have not attempted to share code between the two ownP compatibility layers. (I'm sharing the branch now to discuss Janno's suggestion.)

Merge request reports