University of Twente Student Theses

Login

Formal Automated Verification of a Work-Stealing Deque

Kampen, C.M. van (2020) Formal Automated Verification of a Work-Stealing Deque.

[img] PDF
271kB
Abstract:Multi-core systems brought the possibility for concurrent programs. In task-based parallelism, work-stealing has been an important development. Many designs of a work-stealing framework make use of deques, but they do not properly prove the correctness of the deque. Therefore, the deque from the Lace framework has been implemented and verified for functional correctness using the VerCors verification tool. Under our assumptions, the verification in VerCors passes and shows that all tasks are executed and return the correct result. The verification has been partially validated, but more testing and validation is required before a statement can be made about the validity of the proof.
Item Type:Essay (Bachelor)
Clients:
Unknown organization, Enschede, Netherlands
Faculty:EEMCS: Electrical Engineering, Mathematics and Computer Science
Subject:54 computer science
Programme:Computer Science BSc (56964)
Keywords:Concurrency, Task-based parallelism, Deque, Work-stealing, Deductive verification, VerCors
Link to this item:http://purl.utwente.nl/essays/80687
Export this item as:BibTeX
EndNote
HTML Citation
Reference Manager

 

Repository Staff Only: item control page