A Symbolic Approach to Permission Accounting for Concurrent Reasoning

Marieke Huisman, Wojciech Mostowski

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    5 Citations (Scopus)
    12 Downloads (Pure)

    Abstract

    Permission accounting is fundamental to modular, thread-local reasoning about concurrent programs. This paper presents a new, symbolic system for permission accounting. In existing systems, permissions are numeric value-based and refer to the current thread only. Our system is based on symbolic expressions that provide a view of permissions for all relevant threads in the scope of the permission originator - current thread or a lock. This enables: (a) better understanding of permission tracking for the specifier, (b) more natural specification of complex permission transfer scenarios, and (c) more efficient reasoning for verification tools (in particular, no reasoning about rational numbers is required). Our system is based on symbolic permission slicing to divide permissions between multiple owners, and on tracking the history of permission transfers by means of "I-owe-you" chains of permission owners. We axiomatised our permission system in the KeY verifier as well as in PVS, and proved correct with both tools a list of vital properties about our permissions. KeY is an interactive verification tool for Java and our primary target to employ our permission system. First results with the verification of concurrent Java programs using our permission system in KeY are also reported.
    Original languageUndefined
    Title of host publicationProceedings of the 14th International Symposium on Parallel and Distributed Computing, ISPDC 2015
    Place of PublicationUSA
    PublisherIEEE Computer Society
    Pages165-174
    Number of pages10
    ISBN (Print)978-1-4673-7148-3
    DOIs
    Publication statusPublished - 29 Jun 2015
    Event14th International Symposium on Parallel and Distributed Computing, ISPDC 2015 - St. Raphael Resort, Limassol, Cyprus
    Duration: 29 Jun 20151 Jul 2015
    Conference number: 14
    http://cyprusconferences.org/ispdc2015/

    Publication series

    Name
    PublisherIEEE Computer Society

    Conference

    Conference14th International Symposium on Parallel and Distributed Computing, ISPDC 2015
    Abbreviated titleISPDC 2015
    CountryCyprus
    CityLimassol
    Period29/06/151/07/15
    Internet address

    Keywords

    • EWI-26139
    • Permission accounting
    • fractional permissions
    • IR-98144
    • Formal Specification
    • METIS-314918
    • interactive verification

    Cite this

    Huisman, M., & Mostowski, W. (2015). A Symbolic Approach to Permission Accounting for Concurrent Reasoning. In Proceedings of the 14th International Symposium on Parallel and Distributed Computing, ISPDC 2015 (pp. 165-174). USA: IEEE Computer Society. https://doi.org/10.1109/ISPDC.2015.26