University of Birmingham > Talks@bham > Computer Science Departmental Series > Verifying algorithm correctness on TSO architectures

Verifying algorithm correctness on TSO architectures

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact Mohammad Tayarani.

Host: Behzad Bordbar

Most approaches to verifying linearizability assume a sequentially consistent memory model, which is not always realised in practice. In this paper we study correctness on a {\em weak\/} memory model: the TSO (Total Store Order) memory model, which is implemented in x86 multicore architectures.

Our central result is a proof method that simplifies proofs of linearizability on TSO . This is necessary since the use of local buffers in TSO adds considerably to the verification overhead on top of the already subtle linearizability proofs. The proof method involves constructing a coarse-grained abstraction as an intermediate layer between an abstract description and the concurrent algorithm. This allows the linearizability proof to be split into two smaller components, where the effect of the local buffers in TSO is dealt with at a higher level of abstraction than it would have been otherwise.

This talk is part of the Computer Science Departmental Series series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

Talks@bham, University of Birmingham. Contact Us | Help and Documentation | Privacy and Publicity.
talks@bham is based on talks.cam from the University of Cambridge.