并发程序精化验证及其应用（PPT讲稿）Refinement Verification of Concurrent Programs and Its Applications

Refinement verification of Concurrent Programs and Its Applications Hongjin Liang UniV. of science and technology of china Advisors: Xinyu Feng and Zhong Shao

Refinement Verification of Concurrent Programs and Its Applications Hongjin Liang Univ. of Science and Technology of China Advisors: Xinyu Feng and Zhong Shao

Refinement void main(t void main(t print a square; C print a rectangle; Tcs: t has no more observable behaviors (e.g. lo events by print)than S

Refinement void main() { print a rectangle; } void main() { print a square; }  T  S: T has no more observable behaviors (e.g. I/O events by print) than S

Concurrent Program Refinement Compilers for concurrent programs Multithreaded S Java programs Correct( Compiler) Compiler VS, T. T= Compilers)=TcS Java bytecode

Concurrent Program Refinement • Compilers for concurrent programs T S Compiler Multithreaded Java programs Java bytecode Correct(Compiler): S, T. T = Compiler(S)  T  S

Concurrent Program Refinement Compilers for concurrent programs Fine-grained impl. of concurrent objects(libraries) E.g. javautil.concurrent

Concurrent Program Refinement • Compilers for concurrent programs • Fine-grained impl. of concurrent objects (libraries) – E.g. java.util.concurrent

Concurrent object O Client code c void push(int v)I int po push (7) local b: =false x, t; push (6) X:=new Node(v) x= popo While op: x, next = t b= cas(&top, t, x); Whole program C[OJ How to specify/prove correctness?

Whole program C[O] … push(7); x = pop(); … … push(6); … Client code C Concurrent object O void push(int v) { local b:=false, x, t; x := new Node(v); while (!b) { t := top; x.next = t; b = cas(&top, t, x); } } … int pop() { … … } How to specify/prove correctness?

Correctness of concurrent objects Lineariza bility (herlihy &Wing 90) O Slin S: correctness w.r.t. functionality Spec s: abstract object atomic methods Hard to understand/use Equivalent to contextual refinement (Filipovic et al. J -o Ctx s iff VC. clo] cc[s

Correctness of Concurrent Objects • Linearizability [Herlihy&Wing’90] – O lin S : correctness w.r.t. functionality – Spec S : abstract object (atomic methods) – Hard to understand/use • Equivalent to contextual refinement [Filipovic et al.] – O ctxt S iff C. C[O]  C[S]

O Ctx s iff VC. clo]c cs Concrete void push(int v) obj. O Client C int popo t X y: pop( push(x);‖pint; push Abstract pop obi. S

… x := 7; push( x ); … … y := pop(); print(y); … Client C Concrete obj. O Abstract obj. S void push(int v) { … } int pop() { … } push pop O ctxt S iff C. C[O]  C[S]

Concurrent Program Refinement Compilers for concurrent programs Linearizability of concurrent objects(libraries) Impl. of software transactional memory stm) Atomic block(transaction )> fine-grained impl

Concurrent Program Refinement • Compilers for concurrent programs • Linearizability of concurrent objects (libraries) • Impl. of software transactional memory (STM) – Atomic block (transaction) → fine-grained impl

Concurrent Program Refinement Compilers for concurrent programs Linearizability of concurrent objects(libraries) Impl. of software transactional memory stm) Impl of concurrent garbage collectors (Gc) Impl of operating system(OS) kernels Is such a refinement T c s general enough easy to verify?

Concurrent Program Refinement • Compilers for concurrent programs • Linearizability of concurrent objects (libraries) • Impl. of software transactional memory (STM) • Impl. of concurrent garbage collectors (GC) • Impl. of operating system (OS) kernels Is such a refinement T  S general enough & easy to verify?

Problems withtcs T1 S1 T2 S2 (Compositionality) T1 T2 9 S1 $2 Existing work on verifying TCS: either is not compositional, or limIts applications

(Compositionality) T1 || T2  S1 || S2 T1  S1 T2  S2  Problems with T  S Existing work on verifying T  S : either is not compositional, or limits applications