Conditional Critical Regions We could use a critical region to achieve mutual exclusive access of shared variables. Syntax: (comm)c ::await b then where c is a sequential command(a command with no await and parallel composition). Semantics: Iblboolexp=true(c,o）→*(Skip,r） (await b then c,o）→(skip,o) [Iblboolexp =false (await b then d,o）→(skip;await b then c,) The second rule gives us a"busy-waiting"semantics.If we eliminate that rule,the thread will be blocked when the condition does not hold. Xinyu Feng Shared-Variable Concurrency Conditional Critical Regions We could use a critical region to achieve mutual exclusive access of shared variables. Syntax: (comm) c ::= await b then cˆ where cˆ is a sequential command (a command with no await and parallel composition). Semantics: ~bboolexp σ = true (cˆ, σ) −→∗ (Skip, σ0 ) (await b then cˆ, σ) −→ (Skip, σ0 ) ~bboolexp σ = false (await b then cˆ, σ) −→ (Skip ; await b then cˆ, σ) The second rule gives us a “busy-waiting” semantics. If we eliminate that rule, the thread will be blocked when the condition does not hold. Xinyu Feng Shared-Variable Concurrency