We show how to verify four challenging concurrent finegrained graph-manipulating algorithms, including graph copy, a speculatively parallel Dijkstra, graph marking and spanning tree. We develop a reasoning method for such algorithms that dynamically tracks the contributions and responsibilities of each thread operating on a graph, even in cases of arbitrary recursive thread creation. We demonstrate how to use a logic without abstraction (CoLoSL) to carry out abstract reasoning in the style of iCAP, by building the abstraction into the proof structure rather than incorporating it into the semantic model of the logic.
CITATION STYLE
Raad, A., Hobor, A., Villard, J., & Gardner, P. (2016). Verifying concurrent graph algorithms. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 10017 LNCS, pp. 314–334). Springer Verlag. https://doi.org/10.1007/978-3-319-47958-3_17
Mendeley helps you to discover research relevant for your work.