代写代考 CS 563 Concurrent Programming

CS 563 Concurrent Programming
Lecture 11: Proof of Correctness

Proof of Correctness

Copyright By PowCoder代写 加微信 powcoder

A systematic way to understand and develop concurrent programs based on a programming logic

Predicates {x=0 and y=0} Formulas {P} S {Q}
P, Q are predicates
S is statement
This is called a TRIPLE
P is called the precondition; Q is called the postcondition

Axioms: true formulas (key one is for assignment)
Inference rules — used to construct new (true) formulas; have rules for control statements such as if and do
H1, …, Hn / C
Hi are hypotheses, C is conclusion

A proof is a sequence of lines, each of which is an axiom or can be derived from previous lines by application of inference rules
A theorem is any line in a proof

Interpretation
An interpretation of a logic maps each formula to true or false.

A logic is sound with respect to an interpretation if all its axioms and inference rules are sound
An axiom is sound if it maps to true
An inference rule is sound if its conclusion maps to true when all hypotheses map to true
THEOREMS ⊆ FACTS

Completeness
A logic is complete with respect to an interpretation if a formula that is mapped to true is a theorem,
that is, every formula is provable in the logic
FACTS ⊆ THEOREMS

Computing max of x and y
if (m < y) {m=xandm= y) or (m = y and x < y) } This PROOF OUTLINE captures the essence of what is true at each point; it is an encoding of an actual proof in the programming logic Concurrent Execution { x = 0 and y = 0 } {x=0} {y=0} co x=1; // y=2; oc {x=1} {y=2} { x = 1 and y = 2 } The precondition of the program is the conjunction (and) of the preconditions of the processes. If the processes are disjoint -- as here -- then the "proofs" don't interfere, so the result is the conjunction (and) of the postconditions of the processes. Assertions Predicates that are true at points in a program Interference Statements in one process invalidating assertions in another Interference Arises because of shared variables Example co x = x + 1; // x = x + 2; oc Producer/Consumer Revisited int buf, p = 0, c = 0; {PC:c<=p<=c+1∧a[0:n-1] == A[0:n-1]∧ (p == c+1)⇒(buf == A[p-1])} process Producer { int a[n]; #assume a[i] is initialized to A[i] {IP:PC∧p<=n} while (p < n) { 〈await (p == c);〉 #delay until buf {PC∧p c);〉 #delay until buf full
{IC∧cc}
b[c] = buf; {IC∧cc∧b[c] == A[c]} c=c+1;
{IC∧c==n} }!

Producer/Consumer Revisited
Mutual exclusion
(p==c and p>c) == false
This is an instance of a general method called Exclusion of Configurations
Progress — assuming await statements get a chance
Proving liveness properties requires a stronger logic (e.g., temporal)

Scheduling Policies and Fairness
Most liveness properties depend on fairness
A scheduling policy determines which eligible atomic action to execute next.
Notions of Fairness
Unconditional Fairness: a scheduling policy is unconditionally fair if every unconditional atomic action that is eligible is executed eventually
Weak Fairness: A scheduling policy is weakly fair if 1) it is unconditionally fair, and 2) every conditional atomic action that is eligible is executed eventually, assuming that its condition becomes true and then remains true until is is seen by the process executing the conditional atomic action
Strong Fairness: A scheduling policy is strongly fair if 1) it is unconditionally fair, and 2) every conditional atomic action that is eligible is executed eventually, assuming that its condition is indefinitely often true

int x = 10, y = 0;
co while (x != y) x = x – 1; y = y + 1; // < await (x == y) ; > x = 8; y = 2; oc

int x = 10, c = true;
co c = false;
// while (c) x = x – 1 ;
// while (c) (if (x < 0) x = 10 ; ); oc 程序代写 CS代考 加微信: powcoder QQ: 1823890830 Email: powcoder@163.com