pl/frap
1
0
Fork 0
mirror of https://github.com/achlipala/frap.git synced 2024-12-01 00:26:18 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

SharedMemory chapter: more on operational semantics

Browse source
This commit is contained in:
Adam Chlipala 2016-04-24 19:26:29 -04:00
parent 592c7207bc
commit 545f29c68d
1 changed files with 8 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
frap_book.tex
View file

@ -3412,6 +3412,10 @@ In addition to the basic structure of the languages from the last two chapters,
We follow the common ``threads and locks''\index{locks} style of synchronization, with commands $\mt{Lock} \; a$ and $\mt{Unlock} \; a$ for acquiring and releasing locks, respectively. We follow the common ``threads and locks''\index{locks} style of synchronization, with commands $\mt{Lock} \; a$ and $\mt{Unlock} \; a$ for acquiring and releasing locks, respectively.
We also have $c_1 || c_2$ for running commands $c_1$ and $c_2$ in parallel, giving a scheduler free reign to interleave their atomic steps. We also have $c_1 || c_2$ for running commands $c_1$ and $c_2$ in parallel, giving a scheduler free reign to interleave their atomic steps.
The operational semantics is small-step\index{small-step operational semantics}, especially because big-step semantics\index{big-step operational semantics} is notoriously awkward for concurrency.
Each state of the system is a triple $(h, l, c)$, with $h$ and $c$ the heap and current command from our usual semantics.
New component $l$ is a \emph{lockset}\index{lockset}, recording which locks are currently held, without distinguishing between different threads that might have taken them.
$$\infer{\smallstep{(h, l, x \leftarrow c_1; c_2(x))}{(h', l', x \leftarrow c'_1; c_2(x))}}{ $$\infer{\smallstep{(h, l, x \leftarrow c_1; c_2(x))}{(h', l', x \leftarrow c'_1; c_2(x))}}{
\smallstep{(h, l, c_1)}{(h', l', c'_1)} \smallstep{(h, l, c_1)}{(h', l', c'_1)}
} }
@ -3439,6 +3443,10 @@ This nondeterminism corresponds to the freedom we give to a scheduler\index{sche
Though this kind of concurrent programming is very expressive and often achieves very high performance, it comes at a cost in reasoning, as there may be \emph{exponentially many different schedules} for a single program, measured with respect to the textual length of the program. Though this kind of concurrent programming is very expressive and often achieves very high performance, it comes at a cost in reasoning, as there may be \emph{exponentially many different schedules} for a single program, measured with respect to the textual length of the program.
A popular name for this pitfall is \emph{the state-explosion problem}\index{state-explosion problem}. A popular name for this pitfall is \emph{the state-explosion problem}\index{state-explosion problem}.
Note also that we have omitted any looping constructs from this object language, so all programs terminate.
The Coq formalization uses the mixed-embedding\index{mixed embedding} style, making it not entirely obvious that all programs really do terminate.
In any case, if we must tame the state-explosion problem, we already have our work cut out for us, even when the state space rooted at any concrete state is finite!
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%