A Symbolic Approach to Permission Accounting for Concurrent Reasoning

Marieke Huisman; Wojciech Mostowski

doi:10.1109/ISPDC.2015.26

A Symbolic Approach to Permission Accounting for Concurrent Reasoning

Marieke Huisman, Wojciech Mostowski

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

7 Citations (Scopus)

32 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 language	English
Title of host publication	Proceedings of the 14th International Symposium on Parallel and Distributed Computing, ISPDC 2015
Place of Publication	Piscataway, NJ
Publisher	IEEE
Pages	165-174
Number of pages	10
ISBN (Electronic)	978-1-4673-7148-3
ISBN (Print)	978-1-4673-7147-6
DOIs	https://doi.org/10.1109/ISPDC.2015.26
Publication status	Published - 29 Jun 2015
Event	14th International Symposium on Parallel and Distributed Computing, ISPDC 2015 - St. Raphael Resort, Limassol, Cyprus Duration: 29 Jun 2015 → 1 Jul 2015 Conference number: 14 http://cyprusconferences.org/ispdc2015/

Publication series

Name	Proceedings International Symposium on Parallel and Distributed Computing
Publisher	IEEE
Number	14
Volume	2015
ISSN (Print)	2379-5352

Conference

Conference	14th International Symposium on Parallel and Distributed Computing, ISPDC 2015
Abbreviated title	ISPDC 2015
Country/Territory	Cyprus
City	Limassol
Period	29/06/15 → 1/07/15
Internet address	http://cyprusconferences.org/ispdc2015/

Keywords

Permission accounting
Fractional permissions
Formal specification
Interactive verification
2024 OA procedure

Access to Document

10.1109/ISPDC.2015.26

ArticleFinal published version, 210 KBLicence: Taverne

Cite this

@inproceedings{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 = "Permission accounting, Fractional permissions, Formal specification, Interactive verification, 2024 OA procedure",

author = "Marieke Huisman and Wojciech Mostowski",

year = "2015",

month = jun,

day = "29",

doi = "10.1109/ISPDC.2015.26",

language = "English",

isbn = "978-1-4673-7147-6",

series = "Proceedings International Symposium on Parallel and Distributed Computing",

publisher = "IEEE",

number = "14",

pages = "165--174",

booktitle = "Proceedings of the 14th International Symposium on Parallel and Distributed Computing, ISPDC 2015",

address = "United States",

note = "14th International Symposium on Parallel and Distributed Computing, ISPDC 2015, ISPDC 2015 ; Conference date: 29-06-2015 Through 01-07-2015",

url = "http://cyprusconferences.org/ispdc2015/",

}

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. Proceedings International Symposium on Parallel and Distributed Computing, no. 14, vol. 2015, IEEE, Piscataway, NJ, pp. 165-174, 14th International Symposium on Parallel and Distributed Computing, ISPDC 2015, Limassol, Cyprus, 29/06/15. https://doi.org/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. Piscataway, NJ: IEEE, 2015. p. 165-174 (Proceedings International Symposium on Parallel and Distributed Computing; Vol. 2015, No. 14).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - A Symbolic Approach to Permission Accounting for Concurrent Reasoning

AU - Huisman, Marieke

AU - Mostowski, Wojciech

N1 - Conference code: 14

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 - Permission accounting

KW - Fractional permissions

KW - Formal specification

KW - Interactive verification

KW - 2024 OA procedure

U2 - 10.1109/ISPDC.2015.26

DO - 10.1109/ISPDC.2015.26

M3 - Conference contribution

SN - 978-1-4673-7147-6

T3 - Proceedings International Symposium on Parallel and Distributed Computing

SP - 165

EP - 174

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

PB - IEEE

CY - Piscataway, NJ

T2 - 14th International Symposium on Parallel and Distributed Computing, ISPDC 2015

Y2 - 29 June 2015 through 1 July 2015

ER -

A Symbolic Approach to Permission Accounting for Concurrent Reasoning

Abstract

Publication series

Conference

Keywords

Access to Document

Fingerprint

Cite this