Abstract
We show how to verify four challenging concurrent fine-grained 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 (
) 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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
stipulates that PCMs satisfy the cross-split property [8], which ours do.
stipulates that PCMs satisfy the cross-split property [References
Bornat, R., Calcagno, C., O’Hearn, P.: Local reasoning, separation and aliasing. In: SPACE, vol. 4 (2004)
Dijkstra, E.W., Lamport, L., Martin, A.J., Scholten, C.S., Steffens, E.F.M.: On-the-fly darbage collection: an exercise in cooeration. In: Bauer, F.L., Dijkstra, E.W., Ershov, A., Griffiths, M., Hoare, C.A.R., Wulf, W.A., Samelson, K. (eds.) Language Hierarchies and Interfaces. LNCS, vol. 46, pp. 43–56. Springer, Heidelberg (1976). doi:10.1007/3-540-07994-7_48
Dinsdale-Young, T., Birkedal, L., Gardner, P., Parkinson, M., Yang, H.: Views: compositional reasoning for concurrent programs. In: POPL, pp. 287–300 (2013)
Dinsdale-Young, T., Dodds, M., Gardner, P., Parkinson, M., Vafeiadis, V.: Concurrent abstract predicates. In: ECOOP, pp. 504–528 (2010)
Dockins, R., Hobor, A., Appel, A.: A fresh look at separation algebras and share accounting. In: APLAS (2009)
Feng, X.: Local rely-guarantee reasoning. In: POPL, pp. 315–327 (2009)
Grama, A., Anshul, G., Karypis, G., Kumar, V.: Introduction to Parallel Computing, 2nd edn. Addison Wesley, Boston (2003)
Hobor, A., Villard, J.: The ramifications of sharing in data structures. In: Giacobazzi, R., Cousot, R. (eds.) POPL, pp. 523–536. ACM (2013)
Nanevski, A., Ley-Wild, R., Sergey, I., Delbianco, G.: Communicating state transition systems for fine-grained concurrent resources. In: ESOP, pp. 290–310 (2014)
Raad, A.: Ph.D. thesis, Imperial College London (2016, to appear)
Raad, A., Hobor, A., Villard, J., Gardner, P.: Verifying concurrent graph algorithms (extended) (2016)
Raad, A., Villard, J., Gardner, P.: CoLoSL: concurrent local subjective logic. In: ESOP, pp. 710–735 (2015)
Reynolds, J.: A short course on separation logic (2003). http://www.cs.cmu.edu/afs/cs.cmu.edu/project/fox-19/member/jcr/wwwaac2003/notes7.ps
Sergey, I., Nanevski, A., Banerjee, A.: Mechanized verification of fine-grained concurrent programs. In: PLDI (2015)
Svendsen, K., Birkedal, L.: Impredicative concurrent abstract predicates. In: ESOP (2014)
Turon, A., Dreyer, D., Birkedal, L.: Unifying refinement and Hoare-style reasoning in a logic for higher-order concurrency. In: ICFP, pp. 377–390 (2013)
Yang, H.: Local reasoning for stateful programs. Ph.D. thesis, University of Illinois (2001)
Acknowledgements
This research was supported by EPSRC programme grants EP/H008373/1 and EP/K008528/1, Yale-NUS College and R-607-265-045-121.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing AG
About this paper
Cite this paper
Raad, A., Hobor, A., Villard, J., Gardner, P. (2016). Verifying Concurrent Graph Algorithms. In: Igarashi, A. (eds) Programming Languages and Systems. APLAS 2016. Lecture Notes in Computer Science(), vol 10017. Springer, Cham. https://doi.org/10.1007/978-3-319-47958-3_17
Download citation
DOI: https://doi.org/10.1007/978-3-319-47958-3_17
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-47957-6
Online ISBN: 978-3-319-47958-3
eBook Packages: Computer ScienceComputer Science (R0)