Modelling and verifying non-blocking algorithms that use dynamically allocated memory Export

@mastersthesis{citeulike:566317, abstract = {This thesis presents techniques for the machine-assisted verification of an important class of concurrent algorithms, called non-blocking algorithms. The notion of linearizability is used as a correctness condition for concurrent implementations of sequential datatypes and the use of forward simulation relations as a proof method for showing linearizability is described. A detailed case study is presented: the attempted verification of a concurrent double-ended queue implementation, the Snark algorithm, using the theorem proving system PVS. This case study allows the exploration of the difficult problem of verifying an algorithm that uses low-level pointer operations over a dynamic data-structure in the presence of concurrent access by multiple processes. During the verification attempt, a previously undetected bug was found in Snark the algorithm. Two possible corrections to this algorithm are presented and their merits discussed. The verification of one of these corrections would require the use of a backward simulation relation. The thesis concludes by describing the reason for this extention to the verification methodology and the use of a hierarchical proof structure to simplify verifications that require backward simulations.}, author = {Doherty, Simon}, citeulike-article-id = {566317}, keywords = {algorithms, dcas, lock-free, nonblocking, simulation, thesis-msc, verification}, posted-at = {2006-03-27 23:44:56}, priority = {0}, school = {Victoria University of Wellington}, title = {Modelling and verifying non-blocking algorithms that use dynamically allocated memory}, year = {2003} }

TY - THES ID - citeulike:566317 L3 - citeulike-article-id:566317 N2 - This thesis presents techniques for the machine-assisted verification of an important class of concurrent algorithms, called non-blocking algorithms. The notion of linearizability is used as a correctness condition for concurrent implementations of sequential datatypes and the use of forward simulation relations as a proof method for showing linearizability is described. A detailed case study is presented: the attempted verification of a concurrent double-ended queue implementation, the Snark algorithm, using the theorem proving system PVS. This case study allows the exploration of the difficult problem of verifying an algorithm that uses low-level pointer operations over a dynamic data-structure in the presence of concurrent access by multiple processes. During the verification attempt, a previously undetected bug was found in Snark the algorithm. Two possible corrections to this algorithm are presented and their merits discussed. The verification of one of these corrections would require the use of a backward simulation relation. The thesis concludes by describing the reason for this extention to the verification methodology and the use of a hierarchical proof structure to simplify verifications that require backward simulations. TI - Modelling and verifying non-blocking algorithms that use dynamically allocated memory PB - Victoria University of Wellington KW - algorithms KW - dcas KW - lock-free KW - nonblocking KW - simulation KW - thesis-msc KW - verification AU - Doherty, Simon PY - 2003/// ER -