Modelling of interfering parallelism
- Assignments operate concurrently on store.
- Result is the set of possible result stores.
- Powerdomain constructions required.
- Resumption semantics (Plotkin):
- Central: concurrent evaluation of C_1 and C_2.
- Problem: how to model concurrent interaction?
- Idea: interleave atomic steps of C_1 and C_2.
Concurrency modeled by interleaving!