Loading...
Please wait, while we are loading the content...
Similar Documents
The Design and Verification of Dynamic-sized Nonblocking Data Structures
| Content Provider | Semantic Scholar |
|---|---|
| Author | Doherty, Simon |
| Copyright Year | 2010 |
| Abstract | Modern computer systems often involve multiple processes o r threads of control that communicate through shared memory. However, the implementati o of correct and efficient data structures that can be shared by several processes is freque ntly challenging. This thesis is concerned with the design and verification of a class of share d m mory algorithms known asnonblocking algorithms , which are implementations of shared data structures that p rovide strong progress guarantees. Nonblocking algorithms offer an appealing alternative to traditional techniques for the implementation of shared memor y data structures, but they are difficult to design, and extant algorithms can often be appli ed in only a limited range of systems. Furthermore, because of their subtlety, it is notorio usly difficult to determine whether a given nonblocking algorithm is correct. This thesis addresses these difficulties in two ways. First, we present techniques for the verification of nonblocking algorithms that dynamically al locate memory. These techniques allow the construction of formal and complete proofs of corr ectness, so that each proof may be checked by a mechanical proof assistant. Applying techni ques first developed for the verification of distributed algorithms, we use labelled-tr ansition systems to model algorithms and their specifications, and simulation relations to prove that an implementation meets its specification. Nonblocking algorithms often require a part icular notion of simulation, called backward simulation , that is rarely necessary in other contexts. This thesis con tributes to the relatively limited collective experience in the use of back ward simulation. The second set of contributions addresses the limitations o f many extant nonblocking algorithms. While many nonblocking algorithms allocate me mory dynamically, it is difficult to determine in a nonblocking context when it is safe to free m mory. We present techniques to accomplish this. Furthermore, many nonblocking algorit hms depend on the availability of two powerful synchronisation primitives, known as load-linkedandstore-conditional , which are not normally provided by hardware. We present implement ations of these primitives that work on commonly available platforms. |
| File Format | PDF HTM / HTML |
| Alternate Webpage(s) | http://researcharchive.vuw.ac.nz/xmlui/bitstream/handle/10063/1239/thesis.pdf?sequence=1 |
| Language | English |
| Access Restriction | Open |
| Content Type | Text |
| Resource Type | Article |
