University of Twente Student Theses
Formal Automated Verification of a Work-Stealing Deque
Kampen, C.M. van (2020) Formal Automated Verification of a Work-Stealing Deque.
|
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) |
| 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: | https://purl.utwente.nl/essays/80687 |
| Export this item as: | BibTeX EndNote HTML Citation Reference Manager |
Show download statistics for this publication
Show download statistics for this publicationRepository Staff Only: item control page
