A Symbolic Approach to Permission Accounting for Concurrent Reasoning

Marieke Huisman, Wojciech Mostowski

  • 3 Citations

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
StatePublished - 29 Jun 2015

Publication series

Name
PublisherIEEE Computer Society

Fingerprint

Permission
Java
Fundamental
Scenarios

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. DOI: 10.1109/ISPDC.2015.26

Huisman, Marieke; Mostowski, Wojciech / A Symbolic Approach to Permission Accounting for Concurrent Reasoning.

Proceedings of the 14th International Symposium on Parallel and Distributed Computing, ISPDC 2015. USA : IEEE Computer Society, 2015. p. 165-174.

Research output: Scientific - peer-reviewConference contribution

@inbook{ab2d6e54f00f4e30870a0c180bc1eb2c,
title = "A Symbolic Approach to Permission Accounting for Concurrent Reasoning",
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.",
keywords = "EWI-26139, Permission accounting, fractional permissions, IR-98144, Formal Specification, METIS-314918, interactive verification",
author = "Marieke Huisman and Wojciech Mostowski",
note = "eemcs-eprint-26139",
year = "2015",
month = "6",
doi = "10.1109/ISPDC.2015.26",
isbn = "978-1-4673-7148-3",
publisher = "IEEE Computer Society",
pages = "165--174",
booktitle = "Proceedings of the 14th International Symposium on Parallel and Distributed Computing, ISPDC 2015",
address = "United States",

}

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. IEEE Computer Society, USA, pp. 165-174. DOI: 10.1109/ISPDC.2015.26

A Symbolic Approach to Permission Accounting for Concurrent Reasoning. / Huisman, Marieke; Mostowski, Wojciech.

Proceedings of the 14th International Symposium on Parallel and Distributed Computing, ISPDC 2015. USA : IEEE Computer Society, 2015. p. 165-174.

Research output: Scientific - peer-reviewConference contribution

TY - CHAP

T1 - A Symbolic Approach to Permission Accounting for Concurrent Reasoning

AU - Huisman,Marieke

AU - Mostowski,Wojciech

N1 - eemcs-eprint-26139

PY - 2015/6/29

Y1 - 2015/6/29

N2 - 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.

AB - 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.

KW - EWI-26139

KW - Permission accounting

KW - fractional permissions

KW - IR-98144

KW - Formal Specification

KW - METIS-314918

KW - interactive verification

U2 - 10.1109/ISPDC.2015.26

DO - 10.1109/ISPDC.2015.26

M3 - Conference contribution

SN - 978-1-4673-7148-3

SP - 165

EP - 174

BT - Proceedings of the 14th International Symposium on Parallel and Distributed Computing, ISPDC 2015

PB - IEEE Computer Society

ER -

Huisman M, Mostowski W. A Symbolic Approach to Permission Accounting for Concurrent Reasoning. In Proceedings of the 14th International Symposium on Parallel and Distributed Computing, ISPDC 2015. USA: IEEE Computer Society. 2015. p. 165-174. Available from, DOI: 10.1109/ISPDC.2015.26