Transcript PPT - NUS School of Computing

Oracle Semantics
Aquinas Hobor
Lipton, Perlis, DeMillo 1977
Why Proofs about Code are Hard
Math proofs tend to have the form
If A, then B
2
Lipton, Perlis, DeMillo 1977
Why Proofs about Code are Hard
Math proofs tend to have the form
If A, then B
Proofs about real programs have the form
If A1 and A2 and A3 and A4 and A5…
3
Lipton, Perlis, DeMillo 1977
Why Proofs about Code are Hard
Math proofs tend to have the form
If A, then B
Proofs about real programs have the form
If A1 and A2 and A3 and A4 and A5, then
B1 and B2 and B3
4
Lipton, Perlis, DeMillo 1977
Why Proofs about Code are Hard
Math proofs tend to have the form
If A, then B
Proofs about real programs have the form
If A1 and A2 and A3 and A4 and A5, then
B1 and B2 and B3, except when
C1 or C2 or C3 or C4
5
Lipton, Perlis, DeMillo 1977
Why Proofs about Code are Hard
Math proofs tend to have the form
If A, then B
Proofs about real programs have the form
If A1 and A2 and A3 and A4 and A5, then
B1 and B2 and B3, except when
C1 or C2 or C3 or C4, assuming
D1 and (D2 or D3)
6
Why Proofs about Code are Hard
Two choices:
A) Prove something on paper about a simplification of
the core ideas / algorithm
Problem: actual implementation will have bugs
B) Prove something about the actual code
Problem: too hard to do by hand
7
Machine-Checked Proofs
Solution:
Use computer to check your proofs (we use Coq)
Ideally the computer can help prove as well
Issue:
Machine-checked proofs are large and very timeconsuming to write
Proof engineering becomes a real issue
8
Goal for Oracle Semantics
We want to add concurrency to large, realistic
systems in a provably correct, modular way
Those systems may already exist in a sequential
form; we would like to re-use existing code and
machine-checked proofs wherever possible
The key is to isolate the sequential and concurrent
reasoning from each other.
9
Leroy, 2006
CompCert Project
Sequential
Source Program
(C minor)
Sequential C minor
Operational Semantics
CompCert
Compiler
Sequential
Target Program
(Power PC)
User
Sequential
Translation Correctness
Guarantee
Leroy
Sequential PowerPC
Operational Semantics
10
Leroy, 2006
CompCert Project
Sequential
Source Program
(C minor)
What is relationship here?
Sequential C minor
Operational Semantics
CompCert
Compiler
Sequential
Target Program
(Power PC)
User
Sequential
Translation Correctness
Guarantee
Leroy
Sequential PowerPC
Operational Semantics
11
Appel & Blazy, 2007
Separation Logic for C minor
Sequential
Source Program
(C minor)
Axiomatic Semantics
(Separation Logic)
Program
Verification
Sequential C minor
Operational Semantics
Soundness
Proof
CompCert
Compiler
Sequential
Target Program
(Power PC)
User
Sequential
Translation Correctness
Guarantee
Leroy
Appel & Blazy
Sequential PowerPC
Operational Semantics
12
Changes Required for Concurrency
Concurrent
Source Program
(C minor)
Axiomatic Semantics
(Concurrent
Separation Logic)
Program
Verification
Concurrent C minor
Operational Semantics
Soundness
Proof
Concurrency-Aware
CompCert
Compiler
Concurrent
Target Program
(Power PC)
User
Concurrent
Translation Correctness
Guarantee
Future Work
Concurrent PowerPC
Operational Semantics
This work (Hobor, Appel, & Zappa Nardelli) 13
What this would mean
We would have machine-checked end-to-end
correctness proofs of concurrent programs
Since everything would be machine-checked, we
would have very high assurance that the actual
code running on the hardware had the correct,
expected behavior.
14
Changes Required for Concurrency
Concurrent
Source Program
(C minor)
Axiomatic Semantics
(Concurrent
Separation Logic)
Program
Verification
Concurrent C minor
Operational Semantics
Soundness
Proof
Concurrency-Aware
CompCert
Compiler
Concurrent
Target Program
(Power PC)
User
Concurrent
Translation Correctness
Guarantee
Future Work
Concurrent PowerPC
Operational Semantics
This work (Hobor, Appel, & Zappa Nardelli) 15
Additions to C minor language
We add five new statements:
lock e
lock a lock
unlock e
unlock a lock
makelock e R turn an address into a lock
freelock e
restore an address
fork e el
start a new thread
16
Additions to C minor language
We add five new statements:
lock e
lock a lock
unlock e
unlock a lock
makelock e R turn an address into a lock
freelock e
restore an address
fork e el
start a new thread
Resource Invariant – Describes what resources a thread
acquires on lock and relinquishes on unlock
17
Example Program
[l] := 0;
makelock l (∃y. x ↦ y+y);
[x] := 0;
unlock l;
fork child(l);
lock l;
[x] := [x] + 1;
[x] := [x] + 1;
unlock l;
18
Modularity Principle
Sequential Features
s1 ; s2
if e then s1 else s2
while e do s
break n
(x1, …, xn) := e (e1, …, em)
return (e1, …, en)
x := e
[e1] := e2
Skip
…
Concurrent Features
lock e
unlock e
fork e (e1, …, en)
makelock e R
freelock e
…
19
Modularity Principle
Sequential Features
s1 ; s2
if e then s1 else s2
while e do s
break n
(x1, …, xn) := e (e1, …, em)
return (e1, …, en)
x := e
[e1] := e2
Skip
Connection
…
Concurrent Features
lock e
unlock e
fork e (e1, …, en)
makelock e R
freelock e
…
Easy – Just Syntax
20
Changes Required for Concurrency
Concurrent
Source Program
(C minor)
Axiomatic Semantics
(Concurrent
Separation Logic)
Program
Verification
Concurrent C minor
Operational Semantics
Soundness
Proof
Concurrency-Aware
CompCert
Compiler
Concurrent
Target Program
(Power PC)
User
Concurrent
Translation Correctness
Guarantee
Future Work
Concurrent PowerPC
Operational Semantics
This work (Hobor, Appel, & Zappa Nardelli) 21
Modularity Principle
Sequential Reasoning
Concurrent Reasoning
Sequential Separation Logic
Soundness
Concurrent Separation
Logic Soundness
Sequential Compiler
Correctness
Concurrent Compiler
Correctness
Type Systems
Synchronization
…
…
22
Modularity Principle
Sequential Reasoning
Concurrent Reasoning
Sequential Separation Logic
Soundness
Concurrent Separation
Logic Soundness
Sequential Compiler
Correctness
Concurrent Compiler
Correctness
Type Systems
Synchronization
…
…
Insert Magic Here
23
How is it done?
Key: only consider well-synchronized programs
– Mutual exclusion via Dijkstra Semaphores
– Data-race free
Our operational semantics gets stuck on
ill-synchronized programs
24
Changes to Pure Sequential Semantics
C minor small-step sequential semantics
step relation: (1, 1) ↦ (2, 2)
 = (ρ, m)
 is a control stack
Resource map-aware C minor sequential semantics
step relation: (1, 1) ↦ (2, 2)
 = (ρ, , m)
 is a map from addresses to resources
25
Resources
Basic resources:
| NONE
| VAL
| LOCK of invariant
(data)
(invariant comes from makelock)
Get stuck if you use memory without ownership
Thread resource maps are disjoint – at any time, only one
thread can access each address
Sequential instructions and proofs ignore LOCK
26
Concurrent Operational Semantics
Concurrent C minor step relation
(1, K1, m1, G1) ⇒ (2, K2, m2, G2)
 is scheduler
K is thread list (ρ1, 1, 1) :: (ρ2, 2, 2) :: …
m is memory
G is global resource map – owner of unlocked locks
To execute a sequential instruction, use the resource
map-aware sequential step relation
27
Concurrent Instructions
• The concurrent step executes concurrent
instructions directly
– Updates memory at the lock instruction
– Maintains thread list
– Transfers resources between threads and global pool
• unlock: resources transferred to global pool
• lock:
resources transferred from global pool
28
Space
Time
Thread A
1

R
Thread B
2
Global Resource Map
3
Memory
unlock 𝓁
1
2

R
3
Memory
lock 𝓁
1

R
2
3
Memory
R is the unique resource map that satisfies l’’s lock invariant
29
Avoiding Race Conditions in Semantics
(ρ, lock, m) ⊩ l ⇝ P
m(l) = 0
’  lock = 
Ki = (ρ, , (unlock l) • )
(ρ, lock, m) ⊩ ⊳P
m’ = [l ↦ 1] m
G  lock = G’
K’ = [i -> (ρ, ’, )] K
Unlock
(i :: , K, m, G) ⇒ (, K’, m’, G’)
Does not prevent compilation!
30
Avoiding Race Conditions in Semantics
(ρ, lock, m) ⊩ l ⇝ P
m(l) = 0
’  lock = 
Ki = (ρ, , (unlock l) • )
(ρ, lock, m) ⊩ ⊳P
m’ = [l ↦ 1] m
G  lock = G’
K’ = [i -> (ρ, ’, )] K
Unlock
(i :: , K, m, G) ⇒ (, K’, m’, G’)
Does not prevent compilation!
31
Avoiding Race Conditions in Semantics
(ρ, lock, m) ⊩ l ⇝ P
m(l) = 0
’  lock = 
Ki = (ρ, , (unlock l) • )
(ρ, lock, m) ⊩ ⊳P
m’ = [l ↦ 1] m
G  lock = G’
K’ = [i -> (ρ, ’, )] K
Unlock
(i :: , K, m, G) ⇒ (, K’, m’, G’)
Does not prevent compilation!
32
Avoiding Race Conditions in Semantics
(ρ, lock, m) ⊩ l ⇝ P
m(l) = 0
’  lock = 
Ki = (ρ, , (unlock l) • )
(ρ, lock, m) ⊩ ⊳P
m’ = [l ↦ 1] m
G  lock = G’
K’ = [i -> (ρ, ’, )] K
Unlock
(i :: , K, m, G) ⇒ (, K’, m’, G’)
Does not prevent compilation!
33
Avoiding Race Conditions in Semantics
(ρ, lock, m) ⊩ l ⇝ P
m(l) = 0
’  lock = 
Ki = (ρ, , (unlock l) • )
(ρ, lock, m) ⊩ ⊳P
m’ = [l ↦ 1] m
G  lock = G’
K’ = [i -> (ρ, ’, )] K
Unlock
(i :: , K, m, G) ⇒ (, K’, m’, G’)
Operational semantics is nonconstructive!
34
Avoiding Race Conditions in Semantics
(ρ, lock, m) ⊩ l ⇝ P
m(l) = 0
’  lock = 
Ki = (ρ, , (unlock l) • )
(ρ, lock, m) ⊩ ⊳P
m’ = [l ↦ 1] m
G  lock = G’
K’ = [i -> (ρ, ’, )] K
Unlock
(i :: , K, m, G) ⇒ (, K’, m’, G’)
Operational semantics is nonconstructive!
35
Avoiding Race Conditions in Semantics
(ρ, lock, m) ⊩ l ⇝ P
m(l) = 0
’  lock = 
Ki = (ρ, , (unlock l) • )
(ρ, lock, m) ⊩ ⊳P
m’ = [l ↦ 1] m
G  lock = G’
K’ = [i -> (ρ, ’, )] K
Unlock
(i :: , K, m, G) ⇒ (, K’, m’, G’)
Does not prevent compilation!
36
Coroutine Interleaving
Executes sequentially without interleaving
Interleave when we get to concurrent operation
Key: we have well-synchronized programs
37
Reasoning About Concurrency
Most of the time, concurrent programs are
executing sequential code
Proofs about sequential features are hard enough
We don’t want to add the extra complexity of
concurrency when reasoning about sequential code
Idea: why can’t we just pretend it is sequential?
38
Sequential Reasoning
x := x + 1
[y] := 2
lock l
a := [x]
39
Sequential Reasoning
(1, 1)
↦
x := x + 1
(2, 2)
↦
[y] := 2
(3, 3)
lock l
STUCK
a := [x]
40
Oracular Reasoning
(1, 1)
(o1, 1, 1)
(2, 2)
↦
↦
x := x + 1
(o1, 2, 2)
(3, 3)
↦
↦
[y] := 2
(o1, 3, 3)
↦
lock l
(o2, 4, 4)
STUCK
↦
a := [x]
(o2, 5, 5)
41
Oracular Composition
An oracle o is (, K, G)
 is the scheduler
K is the other threads
G is the global resource map
The oracle simulates running all of the other
threads until the scheduler returns control to
this thread
42
Soundness of Oracular Reasoning
Theorem (connection of oracle and concurrent semantics)
If a thread executes in a certain way on the
oracular machine, then it executes in the
same way when executing in the concurrent
machine
43
Changes Required for Concurrency
Concurrent
Source Program
(C minor)
Axiomatic Semantics
(Concurrent
Separation Logic)
Program
Verification
Concurrent C minor
Operational Semantics
Soundness
Proof
Concurrency-Aware
CompCert
Compiler
Concurrent
Target Program
(Power PC)
User
Concurrent
Translation Correctness
Guarantee
Future Work
Concurrent PowerPC
Operational Semantics
This work (Hobor, Appel, & Zappa Nardelli) 44
Floyd, Hoare
Hoare Logic
A Hoare triple is {precondition} command {postcondition}
Example:
{x = 2} x++ {x = 3}
In our setting, the precondition and postcondition are
predicates on state (locals, memory, resource map, …)
In Coq: Definition predicate : Type := state ->
Prop.
A Hoare logic is a set of axioms for deriving valid triples
Example:
{P} c1 {Q}
{Q} c2 {R}
{P} c1;c2 {R}
45
Reynolds, O’Hearn
Separation Logic
Problem: handling pointers
Example: {x ↦ 0 ⋀ y ↦ 0} [x] := 1 {???}
{x ↦ 1 ⋀ y ↦ 0}
{x ↦ 1 ⋀ y ↦ 1}
Solution: Separation
Use “∗” to split propositions into two disjoint halves
Example: {x ↦ 0 ∗ y ↦ 0} [x] := 1 {x ↦ 1 ∗ y ↦ 0}
Enables more local reasoning for programs with pointers
Key rule (Frame):
{P} c {Q}
{P ∗ F} c {Q ∗ F}
46
CSL 1.0 by O’Hearn, 2006
Concurrent Separation Logic 2.0
Extension of separation logic to handle concurrency
Includes all of typical the rules of separation logic
Associate with each lock an invariant R
l⇝R
≡ l is a lock with invariant R
Separation
Logic
Rules for concurrent operations
{l ⇝ R}
lock l
{(l ⇝ R) * R}
{(l ⇝ R) * R}
unlock l
{l ⇝ R}
Concurrent
Separation Logic
Programs proved in CSL are well-synchronized!
47
Space
Time
Thread A
FA
𝓁⇝ R
1
Thread B
FB
R

R
Thread C
2
3
Memory
lock 𝓁
FA
1
unlock 𝓁
𝓁⇝ R

R
R
FB
2
3
Memory
{𝓁 ⇝ R} lock 𝓁 {(𝓁 ⇝ R) ∗ R}
{FA ∗ (𝓁 ⇝ R)} lock 𝓁 {FA ∗ (𝓁 ⇝ R) ∗ R}
(lock rule)
(frame rule)
48
Changes Required for Concurrency
Concurrent
Source Program
(C minor)
Axiomatic Semantics
(Concurrent
Separation Logic)
Program
Verification
Concurrent C minor
Operational Semantics
Soundness
Proof
Concurrency-Aware
CompCert
Compiler
Concurrent
Target Program
(Power PC)
User
Concurrent
Translation Correctness
Guarantee
Future Work
Concurrent PowerPC
Operational Semantics
This work (Hobor, Appel, & Zappa Nardelli) 49
Verification of Example Program
[l] := 0;
makelock l (∃y. x ↦ y+y);
[x] := 0;
unlock l;
fork child(l);
…
lock l;
[x] := [x] + 1;
[x] := [x] + 1;
unlock l;
50
Verification of Example Program
{F * l ⇝ (∃y. x ↦ y+y)}
lock l;
{F * l ⇝ (∃y. x ↦ y+y) * (∃y. x ↦ y+y)}
[x] := [x] + 1;
[x] := [x] + 1;
unlock l;
51
Verification of Example Program
lock l;
{F * l ⇝ (∃y. x ↦ y+y) * (∃y. x ↦ y+y)}
[x] := [x] + 1;
{F * l ⇝ (∃y. x ↦ y+y) * (∃y. x ↦ y+y + 1)}
[x] := [x] + 1;
unlock l;
52
Verification of Example Program
lock l;
[x] := [x] + 1;
{F * l ⇝ (∃y. x ↦ y+y) * (∃y. x ↦ y+y + 1)}
[x] := [x] + 1;
{F * l ⇝ (∃y. x ↦ y+y) * (∃y. x ↦ y+y + 2)}
unlock l;
53
Verification of Example Program
lock l;
[x] := [x] + 1;
{F * l ⇝ (∃y. x ↦ y+y) * (∃y. x ↦ y+y + 1)}
[x] := [x] + 1;
{F * l ⇝ (∃y. x ↦ y+y) * (∃y. x ↦ y+y + 2)}
(∃y. x ↦ y+y)
unlock l;
54
Verification of Example Program
lock l;
[x] := [x] + 1;
{F * l ⇝ (∃y. x ↦ y+y) * (∃y. x ↦ y+y + 1)}
[x] := [x] + 1;
{F * l ⇝ (∃y. x ↦ y+y) * (∃y. x ↦ y+y)}
unlock l;
55
Verification of Example Program
lock l;
[x] := [x] + 1;
[x] := [x] + 1;
{F * l ⇝ (∃y. x ↦ y+y) * (∃y. x ↦ y+y)}
unlock l;
{F * l ⇝ (∃y. x ↦ y+y)}
56
Verification of Example Program
{F * l ⇝ (∃y. x ↦ y+y)}
lock l;
{F * l ⇝ (∃y. x ↦ y+y) * (∃y. x ↦ y+y)}
[x] := [x] + 1;
{F * l ⇝ (∃y. x ↦ y+y) * (∃y. x ↦ y+y + 1)}
[x] := [x] + 1;
{F * l ⇝ (∃y. x ↦ y+y) * (∃y. x ↦ y+y + 2)}
{F * l ⇝ (∃y. x ↦ y+y) * (∃y. x ↦ y+y)}
unlock l;
{F * l ⇝ (∃y. x ↦ y+y)}
57
Verification of Example Program
{x ↦ _ * l ↦ _}
[l] := 0;
{x ↦ _ * l ↦ 0}
makelock l (∃y. x ↦ y+y);
{x ↦ _ * l ⇝ (∃y. x ↦ y+y)}
[x] := 0;
{x ↦ 0 * l ⇝ (∃y. x ↦ y+y)}
{x ↦ (∃y. x ↦ y+y) * l ⇝ (∃y. x ↦ y+y)}
unlock l;
{l ⇝ (∃y. x ↦ y+y)}
fork child(l);
{l ⇝ (∃y. x ↦ y+y)}
lock l;
{l ⇝ (∃y. x ↦ y+y) * (∃y. x ↦ y+y)}
[x] := [x] + 1;
{l ⇝ (∃y. x ↦ y+y) * (∃y. x ↦ y+y + 1)}
[x] := [x] + 1;
{l ⇝ (∃y. x ↦ y+y) * (∃y. x ↦ y+y + 2)}
{l ⇝ (∃y. x ↦ y+y) * (∃y. x ↦ y+y)}
unlock l;
{l ⇝ (∃y. x ↦ y+y)}
58
Lessons
{x ↦ _ * l ↦ _}
[l] := 0;
{x ↦ _ * l ↦ 0}
makelock l (∃y. x ↦ y+y);
{x ↦ _ * l ⇝ (∃y. x ↦ y+y)}
[x] := 0;
{x ↦ 0 * l ⇝ (∃y. x ↦ y+y)}
{x ↦ (∃y. x ↦ y+y) * l ⇝ (∃y. x ↦ y+y)}
unlock l;
{l ⇝ (∃y. x ↦ y+y)}
fork child(l);
{l ⇝ (∃y. x ↦ y+y)}
lock l;
{l ⇝ (∃y. x ↦ y+y) * (∃y. x ↦ y+y)}
[x] := [x] + 1;
{l ⇝ (∃y. x ↦ y+y) * (∃y. x ↦ y+y + 1)}
[x] := [x] + 1;
{l ⇝ (∃y. x ↦ y+y) * (∃y. x ↦ y+y + 2)}
{l ⇝ (∃y. x ↦ y+y) * (∃y. x ↦ y+y)}
unlock l;
{l ⇝ (∃y. x ↦ y+y)}
A) Many details!
(Actually, some omitted!)
B) Machine-checking is key
C) Has been done for larger
example programs (in Coq)
D) Machine-generation would be
very helpful
59
Changes Required for Concurrency
Concurrent
Source Program
(C minor)
Axiomatic Semantics
(Concurrent
Separation Logic)
Program
Verification
Concurrent C minor
Operational Semantics
Soundness
Proof
Concurrency-Aware
CompCert
Compiler
Concurrent
Target Program
(Power PC)
User
Concurrent
Translation Correctness
Guarantee
Future Work
Concurrent PowerPC
Operational Semantics
This work (Hobor, Appel, & Zappa Nardelli) 60
Difficulties in modeling
Invariants need to be able to refer to other invariants
– Example: 50 ⇝ ∃l2. ((51 ↦ l2) ∗ (l2 ⇝ (∃x.l2+1 ↦ 2*x)
100
lock
101
even
123
lock
124
even
61
Difficulties in modeling
Invariants need to be able to refer to other invariants
– Example: 50 ⇝ ∃l2. ((51 ↦ l2) ∗ (l2 ⇝ (∃x.l2+1 ↦ 2*x)))
50
lock
51
pointer
100
lock
101
even
123
lock
124
even
Nested Invariants are Difficult to Model
62
A modal substructural logic
When a logical proposition describes when and where
another logical proposition holds, we have a modal logic
To describe approximation use the modal operator later “⊳”
⊳P means P will hold at all greater approximations; maybe not now
Key: Avoids circularity and gives clean induction principle
To describe space use ∗ and the operator fashionably “◯”
P * Q means P and Q hold on disjoint sub resource maps
◯ P means that P holds on all resource maps of equal approximation
63
Appel, Melliès, Richards, & Vouillon ‘07
A semantic model
To build a semantic model of the modal logic, we will
build on the “very modal model” of Appel, Melliès,
Richards, & Vouillon
Unlike in that work, where it was sufficient to have only
modal relationships, we also need to spatial properties
In general, we find that semantic models (as opposed
to syntactic techniques) scale better in large systems
64
Shallow Embedding
Invariants are semantic and shallowly embedded in Coq
The shallow embedding means that our invariants are easy to
use and reason about in Coq
We use the same tactics at both the Coq-level and the
invariant-level reasoning
We avoid messy reasoning about binders (that is, the
POPLmark challenge quagmire)
This significantly simplifies the engineering work
65
Another modeling difficulty
We want to embed our semantic assertions directly in
program syntax (for makelock)
Thus, the definitions for program syntax depend on the
definition of predicate
On the other hand, we want to allow a predicate to be
able to specify a function (i.e. f : {P} {Q})
But a this is a predicate about function behavior…
which of course is defined using program syntax
66
A modal definition of a Hoare triple
The solution:
Define our Hoare triple using our modal logic
Thus, a Hoare triple becomes a predicate on state
just like any other predicate
Hypothesis: this will allow us to verify selfmodifying code, such as a JIT
67
(Just a little bit tricky…)
Record semaxArg :Type := SemaxArg {
sa_G: predicate;
sa_R: list val -> predicate;
sa_B: nat -> predicate;
sa_P: predicate;
sa_c: stmt;
sa_Q: predicate
}.
Definition stackframe_of (f : function) : predicate :=
Assert.stackframe f.(fn_stackspace).
Definition prepost_match_sig (P Q : predicate) (sig: signature) : predicate :=
match sig with mksignature args ret =>
|> match_sig1 P args && |> match_sig1 Q ret
end.
Definition bind_args (ids: list ident) (P: predicate) : predicate :=
fun st => exists vl, exists locals,
list_norepet (locals ++ ids) /\ eqv_env (st_rho st) (set_locals locals (set_params vl
ids))
/\ validate P (st_upd_rho (Assert.vl2env vl) st).
Definition claims psi (G P: predicate) : predicate :=
#!(in_prog psi && G --> TT * !(in_prog psi --> P)).
Parameter semax': predicate -> (list val -> predicate) -> (nat -> predicate) ->
predicate -> stmt -> predicate -> predicate.
Definition semax G R B P c Q := forall st, semax' G R B P c Q st.
Definition fun_id (id: ident) (sh: Share.t) (A: Type) (P Q : A -> predicate) : predicate
:=
Exists vf, global_id id =# vf ** Assert.fun_assert vf sh A P Q.
Definition believe (psi: genv) (G G': predicate) : predicate :=
All_ id: ident, All_ sh: Share.t, All_ A: Type, All_ P: A -> predicate, All_ Q: A ->
predicate,
(claims psi G' (fun_id id sh A P Q)) >=>
Ex_ b: block, Ex_ f: function,
prop (Genv.find_symbol psi id = Some b /\ Genv.find_funct_ptr psi b = Some
(Internal f)
/\ list_norepet (f.(fn_vars) ++ f.(fn_params)))
&& All_ x : A,
prepost_match_sig (P x) (Q x) f.(fn_sig)
&& |> semax' G (fun vl => Assert.apply (Q x) vl ** stackframe_of f)
Assert.assert_env_nil
(bind_args f.(fn_params) (P x) ** stackframe_of f)
f.(fn_body) FF.
Definition program_ok psi G := believe psi ([^]G) ([^]G).
Axiom semax_fold_unfold:
semax' = fun G R B P c Q =>
All_ psi: genv, program_ok psi G -->
All_ k: control, All_ F: predicate,
rguard psi (gframe G F c) R k -->
bguard psi (gframe G F c) B k -->
guard psi (gframe G F c) Q k -->
guard psi (gframe G F c) P (Kseq c k).
68
Proving the Rules of CSL
Key: Prove relative to the Oracle Step
Axioms of sequential separation logic are
proved by machine checked proofs of
Appel & Blazy with only minor modification
Separation
Logic
Appel &
Blazy
Concurrent
Separation Logic
The additional axioms added by Concurrent
Hobor, Appel,
Zappa Nardelli
Separation Logic are able to ignore the
difficulties of sequential control flow and focus
on the truly concurrent behavior
69
Status of Machine Checked Proofs
“As expected, it took longer than expected”
- Hobor, Appel, Zappa Nardelli
About 62k lines of proof script at the moment
“Building such scripts is surprisingly addictive, in
a videogame kind of way…”
- Xavier Leroy
70
Status of Machine Checked Proofs
Definition of the Concurrent Machine
Done
Definition of the Oracular Machine
Done
Definition of Hoare Tuple
Done
Sequential Separation Logic Rules
Done
Concurrent S.L. Rules
95% Done (Unlock)
Oracular Soundness
90% Done (Fork)
71
Future Work
Concurrent
Source Program
(C minor)
Axiomatic Semantics
(Concurrent
Separation Logic)
Program
Verification
Concurrent C minor
Operational Semantics
Soundness
Proof
Concurrency-Aware
CompCert
Compiler
Concurrent
Target Program
(Power PC)
User
Concurrent
Translation Correctness
Guarantee
Future Work
Concurrent PowerPC
Operational Semantics
This work (Hobor, Appel, & Zappa Nardelli) 72
Key For Compiler Modification
Lock predicates only look at memory and resource map
The CompCert compiler is designed so that at
each intermediate level, memory is preserved
Thus, the compiler does not have to modify – or
even understand – the predicates embedded in
the makelock statement
73
Future Work
Concurrent
Source Program
(C minor)
Axiomatic Semantics
(Concurrent
Separation Logic)
Program
Verification
Concurrent C minor
Operational Semantics
Soundness
Proof
Concurrency-Aware
CompCert
Compiler
Concurrent
Target Program
(Power PC)
User
Concurrent
Translation Correctness
Guarantee
Future Work
Concurrent PowerPC
Operational Semantics
This paper (Hobor, Appel, & Zappa Nardelli)74
Weak Memory Models
Real processors do not have our interleaving model
Actually, they don’t interleave at all!
They execute instructions out-of-order, subject to various
kinds of ordering constraints
However, for well-synchronized programs, our simplified
interleaving model is sufficient
75
Future Work
Concurrent
Source Program
(C minor)
Axiomatic Semantics
(Concurrent
Separation Logic)
Program
Verification
Concurrent C minor
Operational Semantics
Soundness
Proof
Concurrency-Aware
CompCert
Compiler
Concurrent
Target Program
(Power PC)
User
Concurrent
Translation Correctness
Guarantee
Future Work
Concurrent PowerPC
Operational Semantics
This paper (Hobor, Appel, & Zappa Nardelli)76
Papers and Related Work
Design and Soundness for Concurrent Separation Logic
Resources, Concurrency, and Local Reasoning
Peter O’Hearn, TCS 375, pp271-307, May 2007
A Semantics for Concurrent Separation Logic
Stephen Brookes, TCS 375, pp227-270, May 2007
Oracle Semantics for Concurrent Separation Logic
Aquinas Hobor, Andrew W. Appel, Francesco Zappa Nardelli
ESOP 2008, pages 353-367
Local reasoning for storable locks and threads
Alexey Gotsman, Josh Berdine, Byron Cook, Noam Rinetzky, and Mooly Sagiv
APLAS'07, pages 19-37
77
Papers and Related Work
Semantic Models & Multimodal Logics
A Very Modal Model of a Modern, Major, General Type System
Andrew W. Appel, Paul-Andre Mellies, Christopher Richards, and Jerome Vouillon
POPL 2007
Multimodal Separation Logic for Reasoning About Operational Semantics
Robert Dockins, Andrew W. Appel, Aquinas Hobor
To appear in MFPS 2008
Comparing Semantic and Syntactic Methods in Mechanized Proof Frameworks
C. J. Bell, Robert Dockins, Aquinas Hobor, Andrew W. Appel, David Walker
Currently submitted for publication
78
Papers and Related Work
Sequential Separation Logic
Separation Logic for Small-step C minor
Andrew W. Appel and Sandrine Blazy
TPHOLs 2007, pages 5-21
Automating Program Verification for CSL
Thread-modular shape analysis
Alexey Gotsman, Josh Berdine, Byron Cook, and Mooly Sagiv
PLDI'07, pages 266-277
Automating Separation Logic for Concurrent C minor
William Mansky
Princeton senior thesis, currently being written up for publication
79
Concurrent C minor Project
Concurrent
Source Program
(C minor)
Axiomatic Semantics
(Concurrent
Separation Logic)
Program
Verification
Concurrent C minor
Operational Semantics
Soundness
Proof
Concurrency-Aware
CompCert
Compiler
Concurrent
Target Program
(Power PC)
User
Concurrent
Translation Correctness
Guarantee
Future Work
Concurrent PowerPC
Operational Semantics
This work (Hobor, Appel, & Zappa Nardelli) 80