Change search
ReferencesLink to record
Permanent link

Direct link
Verification of Work-stealing Deque Implementation
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology.
2012 (English)Independent thesis Advanced level (degree of Master (Two Years)), 20 credits / 30 HE creditsStudent thesis
Abstract [en]

Software verification is the process of checking a software system to make sure it meets its specifications. A software system can be either of sequential or concurrent type. The most important part in a sequential system from the verification point of view is the relationship between the system’s inputs and outputs. More formally, verification of a sequential system can be expressed in the following form: If a program starts in a specific state which satisfies a certain condition(precondition), then it eventually terminates and the program variables at the final state satisfy some given relation with the corresponding values at the beginning of the execution [20]. But the story in verification of concurrent software is different.

Many concurrent software use parallelism in order to make calculations more efficient. Parallelism is used to distribute a large amount of computations between different processing units to finish them in a shorter time. Input and output values are still enough for specifying the behavior of these sequential processes but are absolutely not enough for specifying the behaviors of the concurrent system. This is mainly because of the interactions between processes which can not only be expressed with the help of inputs and outputs.

One important aspect in verification of concurrent programs is to directly verify them against an abstract specification of overall functionality. For example, a concurrent implementation of a familiar data type abstraction, such as a queue, could be verified to conform to a simple abstract specification of such a data type. This has been accomplished for finite-state programs and some verification tools like SPIN [3, 13] are already supporting it, but to our knowledge there are no approaches for handling unbounded data domains in specifications and implementations as is the case for a work-stealing double ended queue(deque) implementation.

In this project we present a technique for automatically verifying that a concurrent workstealing deque conforms to an abstract specification of its functionality and we mathematically prove our technique's correctness. We also demonstrate its use by applying it to a famous implementation of a work-stealing deque data structure presented by Arora, et al. [2]

Place, publisher, year, edition, pages
IT, 12 008
National Category
Engineering and Technology
URN: urn:nbn:se:uu:diva-170127OAI: diva2:508492
Educational program
Master Programme in Computer Science
Available from: 2012-03-08 Created: 2012-03-08 Last updated: 2012-03-08Bibliographically approved

Open Access in DiVA

fulltext(794 kB)528 downloads
File information
File name FULLTEXT01.pdfFile size 794 kBChecksum SHA-512
Type fulltextMimetype application/pdf

By organisation
Department of Information Technology
Engineering and Technology

Search outside of DiVA

GoogleGoogle Scholar
Total: 528 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

Total: 507 hits
ReferencesLink to record
Permanent link

Direct link