CS代考 Separation Logic for

Separation Logic for
Automated Verification A Partial Overview
Toby MD 8.17 (Level 8, Doug McDonell Bldg)
http://people.eng.unimelb.edu.au/tobym @tobycmurray

INTRODUCTION TO SEPARATION LOGIC

Hoare Reasoning
Hoare Triple: {P} prog {Q}
3 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Hoare Reasoning
Hoare Triple: {P} prog {Q}
CONSEQ P ⇒ P’ {P’} prog {Q’} Q’ ⇒ Q {P} prog {Q}
3 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Hoare Reasoning
Hoare Triple: {P} prog {Q}
CONSEQ P ⇒ P’ {P’} prog {Q’} Q’ ⇒ Q {P} prog {Q}
ASSIGN {Q[e/x]} x := e {Q}
Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Hoare Reasoning
Hoare Triple: {P} prog {Q}
CONSEQ P ⇒ P’ {P’} prog {Q’} Q’ ⇒ Q {P} prog {Q}
ASSIGN {Q[e/x]} x := e {Q} For local variables x and y:
{2 = 2 ∧ y = 3} x := 2 {x = 2 ∧ y = 3} (by ASSIGN) {x = 3 ∧ y = 3} x := 2 {x = 2 ∧ y = 3} (by CONSEQ)
Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Hoare Reasoning
Hoare Triple: {P} prog {Q}
CONSEQ P ⇒ P’ {P’} prog {Q’} Q’ ⇒ Q {P} prog {Q}
ASSIGN {Q[e/x]} x := e {Q} For local variables x and y:
{2 = 2 ∧ y = 3} x := 2 {x = 2 ∧ y = 3} (by ASSIGN) {x = 3 ∧ y = 3} x := 2 {x = 2 ∧ y = 3} (by CONSEQ)
(ASSIGN is) valid (only) because x and y cannot alias.
Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Heap Reasoning
What if x and y are pointers into the heap? *x := 2
4 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
Heap Reasoning
What if x and y are pointers into the heap? *x := 2
Maps-ToAssertion: p↦e
“the heap location identified by p holds the value e”
Is this Hoare triple valid?
{x ↦ 3 ∧ y ↦ 3} *x := 2 {x ↦ 2 ∧ y ↦ 3}

Heap Reasoning
What if x and y are pointers into the heap? *x := 2
Maps-ToAssertion: p↦e
“the heap location identified by p holds the value e”
Is this Hoare triple valid?
{x ↦ 3 ∧ y ↦ 3} *x := 2 {x ↦ 2 ∧ y ↦ 3}
Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Global Reasoning
We need a way to reason locally about statements like *x := 2
Hoare predicates like P and Q in {P} prog {Q} talk globally: they hold, or not, for the entire state.
5 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Local Reasoning
Idea: have predicates P characterise the part of the state that they talk about.
6 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Local Reasoning
Idea: have predicates P characterise the part of the state that they talk about.
loci ↦ e loci vali ……
Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Local Reasoning
Idea: have predicates P characterise the part of the state that they talk about.
loci ↦ e loci vali ……
This part is called the predicate’s domain (aka footprint), written dom(P)
Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Local Reasoning
Idea: have predicates P characterise the part of the state that they talk about.
loci ↦ e loci vali ……
This part is called the predicate’s domain (aka footprint), written dom(P)
dom(p ↦ e) = {p}
Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Local Reasoning
A valid triple:
{x↦3} *x := 2 {x↦2}
7 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Local Reasoning
A valid triple:
{x↦3} *x := 2 {x↦2} Any pre-state
satisfying x ↦ 3
Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Local Reasoning
A valid triple:
{x↦3} *x := 2 {x↦2} Any pre-state
satisfying x ↦ 3
Post-State
loc0 val0 loc0 val0
…… ……
…… ……
Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Local Reasoning
A valid triple:
{x↦3} *x := 2 {x↦2} Any pre-state
satisfying x ↦ 3
Post-State
loc0 val0 loc0 val0
…… ……
…… ……
Satisfies x ↦ 2
Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Local Reasoning
A valid triple:
{x↦3} *x := 2 {x↦2} Any pre-state
satisfying x ↦ 3
Post-State
loc0 val0 loc0 val0
…… ……
…… ……
Satisfies x ↦ 2
How do we talk about other parts of the heap? Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Compositional Reasoning
Separating Conjunction: P ⋆ Q
“P holds for its part of the heap and Q holds for its part and,
moreover, those two parts are separate.”
8 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Compositional Reasoning
Separating Conjunction: P ⋆ Q
“P holds for its part of the heap and Q holds for its part and,
moreover, those two parts are separate.” x↦3⋆y↦3
implies that x ≠ y, i.e. x and y do not alias
8 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Compositional Reasoning
Separating Conjunction: P ⋆ Q
“P holds for its part of the heap and Q holds for its part and,
moreover, those two parts are separate.” x↦3⋆y↦3
implies that x ≠ y, i.e. x and y do not alias Is this triple valid?
{x ↦ 3 ⋆ y ↦ 3} *x := 2 {x ↦ 2 ⋆ y ↦ 3}
8 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Compositional Reasoning
Separating Conjunction: P ⋆ Q
“P holds for its part of the heap and Q holds for its part and,
moreover, those two parts are separate.” x↦3⋆y↦3
implies that x ≠ y, i.e. x and y do not alias Is this triple valid?
{x ↦ 3 ⋆ y ↦ 3} *x := 2 {x ↦ 2 ⋆ y ↦ 3} Yes.
8 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

The Frame Rule
{P} prog {Q} modv(prog) ∩ fv(R) = {} {P ⋆ R} prog {Q ⋆ R}
9 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

The Frame Rule
{P} prog {Q} modv(prog) ∩ fv(R) = {} {P ⋆ R} prog {Q ⋆ R}
Allows us to derive
{x ↦ 3 ⋆ y ↦ 3} *x := 2 {x ↦ 2 ⋆ y ↦ 3}
{x↦3} *x := 2 {x↦2}
Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

The Frame Rule
{P} prog {Q} modv(prog) ∩ fv(R) = {} {P ⋆ R} prog {Q ⋆ R}
Allows us to derive
{x ↦ 3 ⋆ y ↦ 3} *x := 2 {x ↦ 2 ⋆ y ↦ 3}
{x↦3} *x := 2 {x↦2}
modv(prog): the set of local variables modified by prog
Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

The Frame Rule
{P} prog {Q} modv(prog) ∩ fv(R) = {} {P ⋆ R} prog {Q ⋆ R}
Allows us to derive
{x ↦ 3 ⋆ y ↦ 3} *x := 2 {x ↦ 2 ⋆ y ↦ 3}
{x↦3} *x := 2 {x↦2}
modv(prog): the set of local variables modified by prog fv(R): the set of free variables mentioned by R
Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

The Frame Rule
{P} prog {Q} modv(prog) ∩ fv(R) = {} {P ⋆ R} prog {Q ⋆ R}
Allows us to derive
{x ↦ 3 ⋆ y ↦ 3} *x := 2 {x ↦ 2 ⋆ y ↦ 3}
{x↦3} *x := 2 {x↦2}
modv(prog): the set of local variables modified by prog fv(R): the set of free variables mentioned by R
modv(*x := 2) = {}
Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

The Frame Rule
{P} prog {Q} modv(prog) ∩ fv(R) = {} {P ⋆ R} prog {Q ⋆ R}
Allows us to derive
{x ↦ 3 ⋆ y ↦ 3} *x := 2 {x ↦ 2 ⋆ y ↦ 3}
{x↦3} *x := 2 {x↦2}
modv(prog): the set of local variables modified by prog fv(R): the set of free variables mentioned by R
modv(*x := 2) = {} fv(y↦3) = {y} Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

The Side Condition
{P} prog {Q} modv(prog) ∩ fv(R) = {} {P ⋆ R} prog {Q ⋆ R}
modv(*x := 2; y := x) = {y} fv(y ↦ 3) = {y}
Side condition doesn’t hold.
10 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

The Side Condition
{P} prog {Q} modv(prog) ∩ fv(R) = {} {P ⋆ R} prog {Q ⋆ R}
Suppose we had:
{x ↦ 3} *x := 2; y := x {x ↦ 2}
modv(*x := 2; y := x) = {y} fv(y ↦ 3) = {y}
Side condition doesn’t hold.
10 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

The Side Condition
{P} prog {Q} modv(prog) ∩ fv(R) = {} {P ⋆ R} prog {Q ⋆ R}
Suppose we had:
{x ↦ 3} *x := 2; y := x {x ↦ 2}
Clearly, it is not the case that:
{x ↦ 3 ⋆ y ↦ 3} *x := 2; y := x {x ↦ 2 ⋆ y ↦ 3}
modv(*x := 2; y := x) = {y} fv(y ↦ 3) = {y}
Side condition doesn’t hold.
10 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Validity of Triples
Meaning of {P} prog {Q} in Separation Logic
11 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Validity of Triples
Meaning of {P} prog {Q} in Separation Logic
Partial Correctness: If P holds initially then whenever prog terminates successfully, then Q holds and, moreover, prog never fails.
11 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Memory Safety
Example: {x = NULL} y := *x {true} Does this triple hold?
12 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
Memory Safety
Example: {x = NULL} y := *x {true} Does this triple hold?
In a language semantics in which all memory-unsafe accesses cause failure,
separation logic guarantees memory safety.

A LITTLE MORE FORMALLY

Expressions, Commands
Expressions: e ::= x | n | …
May mention (local) variables but not the heap.
Are evaluated against a store s :: Var → Int ⟦e⟧s :: Int
14 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
Expressions, Commands
Expressions: e ::= x | n | …
May mention (local) variables but not the heap.
Are evaluated against a store s :: Var → Int ⟦e⟧s :: Int
Commands: c ::= c1 ; c2 | if e then ct else cf | while e do c | x := e
| x := *e | *e1 := e2

Expressions, Commands
Expressions: e ::= x | n | …
May mention (local) variables but not the heap.
Are evaluated against a store s :: Var → Int ⟦e⟧s :: Int
Commands: c ::= c1 ; c2 | if e then ct else cf | while e do c | x := e
| x := *e | *e1 := e2 Note: heap- and store-update are
syntactically distinct.
Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Heap Read Rule (Simplified) x ∉ vars(e)
{e ↦ v} x := *e {x = v ∧ e ↦ v}
15 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Heap Read Rule (Simplified) x ∉ vars(e)
{e ↦ v} x := *e {x = v ∧ e ↦ v} x := *(y+1)
15 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Heap Read Rule (Simplified) x ∉ vars(e)
{e ↦ v} x := *e {x = v ∧ e ↦ v} h
x := *(y+1)
…… ……
15 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Heap Read Rule (Simplified) x ∉ vars(e)
{e ↦ v} x := *e {x = v ∧ e ↦ v} h
x := *(y+1)
…… ……
Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
y+1 ↦ 3 holds

Heap Read Rule (Simplified) x ∉ vars(e)
{e ↦ v} x := *e {x = v ∧ e ↦ v} h
x := *(y+1)
…… ……
…… ……
Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
y+1 ↦ 3 holds

Heap Read Rule (Simplified) x ∉ vars(e)
{e ↦ v} x := *e {x = v ∧ e ↦ v} h
x := *(y+1)
…… ……
…… ……
y+1 ↦ 3 holds
NOTE: We need a more general rule for when x ∈ vars(e)
but that is beyond the scope of today’s lecture
15 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Assignment Rules
HEAPW {e1 ↦_} *e1 := e2 {e1↦e2}
ASSIGN {x ≐ n} x := e {x ≐ e[n/x]}
x ∉ vars(e) {emp} x := e {x ≐ e}
16 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Frame Rule
modv(x := e) = {x}
modv(x := *e) = {x}
modv(*e1 := e2) = {}
modv(while e do c) = modv(c) modv(if e then ct else cf) = modv(ct) ∪ modv(cf)
modv(c1 ; c2) = modv(c1) ∪ modv(c2)
{P} c {Q} modv(c) ∩ fv(R) = {} {P ⋆ R} c {Q ⋆ R}
Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Example Proof
{x↦vx ⋆y↦vy}
*y := t; {x↦vy ⋆y↦vx}
18 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Example Proof
{x↦vx ⋆y↦vy}
*y := t; {x↦vy ⋆y↦vx}
Apply the Hoare sequencing rule
18 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Example Proof
{x↦vx ⋆y↦vy} t := *x;
{(x↦vx ∧t = vx) ⋆ y↦vy}
19 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
{(x↦vx ∧t = vx) ⋆ y↦vy}
*y := t; {x↦vy ⋆y↦vx}

Example Proof
20 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Example Proof
t := *x; {x↦vx ∧t = vx}
20 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Example Proof
t := *x; {x↦vx ∧t = vx}
{x↦vx ⋆y↦vy} t := *x;
{(x↦vx ∧t = vx) ⋆ y↦vy}
20 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Example Proof Outline
{x↦vx ⋆y↦vy} t := *x;
{(x↦vx ∧t = vx) ⋆ y↦vy} u := *y;
{(x ↦ vx ∧ t = vx) ⋆ (y ↦ vy ∧ u = vy)} *x := u;
{(x ↦ u ∧ t = vx) ⋆ (y ↦ vy ∧ u = vy)} *y := t;
{(x↦u∧t = vx) ⋆ (y↦t∧ u = vy)}
21 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Example Proof Outline
{x↦vx ⋆y↦vy} t := *x;
{(x↦vx ∧t = vx) ⋆ y↦vy} u := *y;
{(x ↦ vx ∧ t = vx) ⋆ (

程序代写 CS代考加微信: powcoder QQ: 1823890830 Email: powcoder@163.com

Related Posts