pl/frap
1
0
Fork 0
mirror of https://github.com/achlipala/frap.git synced 2024-11-28 07:16:20 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

Proofreading ConcurrentSeparationLogic

Browse source
This commit is contained in:
Adam Chlipala 2018-05-08 09:13:06 -04:00
parent 7e84adc6bd
commit 0f73a3901c
3 changed files with 8 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
ConcurrentSeparationLogic.v
View file

@ -9,8 +9,8 @@ Set Implicit Arguments.
Set Asymmetric Patterns. Set Asymmetric Patterns.
(* Let's combine the subjects of the last two lectures, to let us prove (* Let's combine the subjects of SeparationLogic and SharedMemory, to let us
* correctness of concurrent programs that do dynamic management of shared * prove correctness of concurrent programs that do dynamic management of shared
* memory. *) * memory. *)
@ -493,7 +493,7 @@ Hint Resolve try_ptsto_first.
(** ** The nonzero shared counter *) (** ** The nonzero shared counter *)
(* This program has two threads shared a numeric counter, which starts out as (* This program has two threads sharing a numeric counter, which starts out as
* nonzero and remains that way, since each thread only increments the counter, * nonzero and remains that way, since each thread only increments the counter,
* with the lock held to avoid race conditions. (Actually, the lock isn't * with the lock held to avoid race conditions. (Actually, the lock isn't
* needed to maintain the property in this case, but it's a pleasant starting * needed to maintain the property in this case, but it's a pleasant starting

2
ConcurrentSeparationLogic_template.v
View file

@ -474,7 +474,7 @@ Hint Resolve try_ptsto_first.
(** ** The nonzero shared counter *) (** ** The nonzero shared counter *)
(* This program has two threads shared a numeric counter, which starts out as (* This program has two threads sharing a numeric counter, which starts out as
* nonzero and remains that way, since each thread only increments the counter, * nonzero and remains that way, since each thread only increments the counter,
* with the lock held to avoid race conditions. *) * with the lock held to avoid race conditions. *)

8
frap_book.tex
View file

@ -3674,7 +3674,7 @@ As a result, our extracted programs achieve the asymptotic performance that we w
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\chapter{Separation Logic} \chapter{Separation Logic}\label{seplog}
In our Hoare-logic examples so far, we have intentionally tread lightly when it comes to the potential aliasing\index{aliasing} of pointer variables in a program. In our Hoare-logic examples so far, we have intentionally tread lightly when it comes to the potential aliasing\index{aliasing} of pointer variables in a program.
Generally, we have only worked with, for instance, a single array at a time. Generally, we have only worked with, for instance, a single array at a time.
@ -4355,7 +4355,7 @@ Therefore, it is natural to give an efficient formula for computing $c'$ in term
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\chapter{Introduction to Reasoning About Shared-Memory Concurrency} \chapter{Introduction to Reasoning About Shared-Memory Concurrency}\label{sharedmem}
Separation logic~\index{separation logic} tames sharing of a mutable memory across libraries and data structures. Separation logic~\index{separation logic} tames sharing of a mutable memory across libraries and data structures.
We will need some additional techniques when we add concurrency to the mix, resulting in the \emph{shared-memory}\index{shared-memory concurrency} style of concurrency. We will need some additional techniques when we add concurrency to the mix, resulting in the \emph{shared-memory}\index{shared-memory concurrency} style of concurrency.
@ -4730,13 +4730,13 @@ This condition effectively forces the ample set for the example program above to
\chapter{Concurrent Separation Logic} \chapter{Concurrent Separation Logic}
The last two chapters respectively introduced techniques for reasoning about two tricky aspects of programs: heap-allocated linked data structures\index{linked data structures} and shared-memory concurrency\index{shared-memory concurrency}. Chapters \ref{seplog} and \ref{sharedmem} respectively introduced techniques for reasoning about two tricky aspects of programs: heap-allocated linked data structures\index{linked data structures} and shared-memory concurrency\index{shared-memory concurrency}.
When we add concurrency to the mix for a program-reasoning problem, we are often surprised at how much more complex it becomes. When we add concurrency to the mix for a program-reasoning problem, we are often surprised at how much more complex it becomes.
This chapter introduces a pleasant exception to the rule, \emph{concurrent separation logic}\index{concurrent separation logic}, a rather small addition to separation logic\index{separation logic} that supports invariant-based reasoning about threads-and-locks shared-memory programs. This chapter introduces a pleasant exception to the rule, \emph{concurrent separation logic}\index{concurrent separation logic}, a rather small addition to separation logic\index{separation logic} that supports invariant-based reasoning about threads-and-locks shared-memory programs.
\section{Object Language: Loops and Locks} \section{Object Language: Loops and Locks}
Here's the object language we adopt, which should be old hat by now, just mixing together features of the object languages from the previous two chapters. Here's the object language we adopt, which should be old hat by now, just mixing together features of the object languages from Chapters \ref{seplog} and \ref{sharedmem}.
$$\begin{array}{rrcl} $$\begin{array}{rrcl}
\textrm{Commands} & c &::=& \mt{Fail} \mid \mt{Return} \; v \mid x \leftarrow c; c \mid \mt{Loop} \; i \; f \\ \textrm{Commands} & c &::=& \mt{Fail} \mid \mt{Return} \; v \mid x \leftarrow c; c \mid \mt{Loop} \; i \; f \\