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 | |
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 |
Keywords
- Permission accounting
- Fractional permissions
- Formal specification
- Interactive verification
- 2024 OA procedure