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

Proofreading SharedMemory

Browse source
This commit is contained in:
Adam Chlipala 2018-05-01 19:59:02 -04:00
parent b74bc4b248
commit df4016a2c3
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
SharedMemory.v
View file

@ -400,7 +400,7 @@ Qed.
* technique to also harness commutativity of operations that *do* depend on the * technique to also harness commutativity of operations that *do* depend on the
* shared state, but in particular controlled ways? Why, yes we can! The most * shared state, but in particular controlled ways? Why, yes we can! The most
* popular such technique from the model-checking world is * popular such technique from the model-checking world is
* *partial order reduction*. *) * *partial-order reduction*. *)
(* First, here's an example where we should be able to do better than allowing (* First, here's an example where we should be able to do better than allowing
* either thread to run in every step, as we model-check. *) * either thread to run in every step, as we model-check. *)