VerCors: A Layered Approach to Practical Verification of Concurrent Software

A. Amighi, Stefan Blom, Marieke Huisman

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

This paper discusses how several concurrent program verification techniques can be combined in a layered approach, where each layer is especially suited to verify one aspect of concurrent programs, thus making verification of concurrent programs practical. At the bottom layer, we use a combination of implicit dynamic frames and CSL-style resource invariants, to reason about data race freedom of programs. We illustrate this on the verification of a lock-free queue implementation. On top of this, layer 2 enables reasoning about resource invariants that express a relationship between thread-local and shared variables. This is illustrated by the verification of a reentrant lock implementation, where thread-locality is used to specify for a thread which locks it holds, while there is a global notion of ownership, expressing for a lock by which thread it is held. Finally, the top layer adds a notion of histories to reason about functional properties. We illustrate how this is used to prove that the lock-free queue preserves the order of elements, without having to reverify the aspects related to data race freedom.
LanguageUndefined
Title of host publicationProceedings of the 24th Euromicro International Conference on Parallel, Distributed, and Network-Based Processing (PDP 2016)
Place of PublicationUSA
PublisherIEEE Computer Society
Pages495-503
Number of pages9
ISBN (Print)978-1-4673-8775-0
DOIs
StatePublished - Feb 2016
Event24th Euromicro International Conference on Parallel, Distributed, and Network-Based Processing, PDP 2016 - Heraklion, Crete, Greece
Duration: 17 Feb 201619 Feb 2016
Conference number: 24

Publication series

Name
PublisherIEEE Computer Society
ISSN (Print)2377-5750

Conference

Conference24th Euromicro International Conference on Parallel, Distributed, and Network-Based Processing, PDP 2016
Abbreviated titlePDP
CountryGreece
CityHeraklion, Crete,
Period17/02/1619/02/16

Keywords

  • EWI-27395
  • Program Verification
  • METIS-320885
  • IR-102859
  • Separation Logic

Cite this

Amighi, A., Blom, S., & Huisman, M. (2016). VerCors: A Layered Approach to Practical Verification of Concurrent Software. In Proceedings of the 24th Euromicro International Conference on Parallel, Distributed, and Network-Based Processing (PDP 2016) (pp. 495-503). USA: IEEE Computer Society. DOI: 10.1109/PDP.2016.107
Amighi, A. ; Blom, Stefan ; Huisman, Marieke. / VerCors: A Layered Approach to Practical Verification of Concurrent Software. Proceedings of the 24th Euromicro International Conference on Parallel, Distributed, and Network-Based Processing (PDP 2016). USA : IEEE Computer Society, 2016. pp. 495-503
@inproceedings{47e67c3c97c14e56bab18ad06feda1ee,
title = "VerCors: A Layered Approach to Practical Verification of Concurrent Software",
abstract = "This paper discusses how several concurrent program verification techniques can be combined in a layered approach, where each layer is especially suited to verify one aspect of concurrent programs, thus making verification of concurrent programs practical. At the bottom layer, we use a combination of implicit dynamic frames and CSL-style resource invariants, to reason about data race freedom of programs. We illustrate this on the verification of a lock-free queue implementation. On top of this, layer 2 enables reasoning about resource invariants that express a relationship between thread-local and shared variables. This is illustrated by the verification of a reentrant lock implementation, where thread-locality is used to specify for a thread which locks it holds, while there is a global notion of ownership, expressing for a lock by which thread it is held. Finally, the top layer adds a notion of histories to reason about functional properties. We illustrate how this is used to prove that the lock-free queue preserves the order of elements, without having to reverify the aspects related to data race freedom.",
keywords = "EWI-27395, Program Verification, METIS-320885, IR-102859, Separation Logic",
author = "A. Amighi and Stefan Blom and Marieke Huisman",
note = "10.1109/PDP.2016.107",
year = "2016",
month = "2",
doi = "10.1109/PDP.2016.107",
language = "Undefined",
isbn = "978-1-4673-8775-0",
publisher = "IEEE Computer Society",
pages = "495--503",
booktitle = "Proceedings of the 24th Euromicro International Conference on Parallel, Distributed, and Network-Based Processing (PDP 2016)",
address = "United States",

}

Amighi, A, Blom, S & Huisman, M 2016, VerCors: A Layered Approach to Practical Verification of Concurrent Software. in Proceedings of the 24th Euromicro International Conference on Parallel, Distributed, and Network-Based Processing (PDP 2016). IEEE Computer Society, USA, pp. 495-503, 24th Euromicro International Conference on Parallel, Distributed, and Network-Based Processing, PDP 2016, Heraklion, Crete, Greece, 17/02/16. DOI: 10.1109/PDP.2016.107

VerCors: A Layered Approach to Practical Verification of Concurrent Software. / Amighi, A.; Blom, Stefan; Huisman, Marieke.

Proceedings of the 24th Euromicro International Conference on Parallel, Distributed, and Network-Based Processing (PDP 2016). USA : IEEE Computer Society, 2016. p. 495-503.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

TY - GEN

T1 - VerCors: A Layered Approach to Practical Verification of Concurrent Software

AU - Amighi,A.

AU - Blom,Stefan

AU - Huisman,Marieke

N1 - 10.1109/PDP.2016.107

PY - 2016/2

Y1 - 2016/2

N2 - This paper discusses how several concurrent program verification techniques can be combined in a layered approach, where each layer is especially suited to verify one aspect of concurrent programs, thus making verification of concurrent programs practical. At the bottom layer, we use a combination of implicit dynamic frames and CSL-style resource invariants, to reason about data race freedom of programs. We illustrate this on the verification of a lock-free queue implementation. On top of this, layer 2 enables reasoning about resource invariants that express a relationship between thread-local and shared variables. This is illustrated by the verification of a reentrant lock implementation, where thread-locality is used to specify for a thread which locks it holds, while there is a global notion of ownership, expressing for a lock by which thread it is held. Finally, the top layer adds a notion of histories to reason about functional properties. We illustrate how this is used to prove that the lock-free queue preserves the order of elements, without having to reverify the aspects related to data race freedom.

AB - This paper discusses how several concurrent program verification techniques can be combined in a layered approach, where each layer is especially suited to verify one aspect of concurrent programs, thus making verification of concurrent programs practical. At the bottom layer, we use a combination of implicit dynamic frames and CSL-style resource invariants, to reason about data race freedom of programs. We illustrate this on the verification of a lock-free queue implementation. On top of this, layer 2 enables reasoning about resource invariants that express a relationship between thread-local and shared variables. This is illustrated by the verification of a reentrant lock implementation, where thread-locality is used to specify for a thread which locks it holds, while there is a global notion of ownership, expressing for a lock by which thread it is held. Finally, the top layer adds a notion of histories to reason about functional properties. We illustrate how this is used to prove that the lock-free queue preserves the order of elements, without having to reverify the aspects related to data race freedom.

KW - EWI-27395

KW - Program Verification

KW - METIS-320885

KW - IR-102859

KW - Separation Logic

U2 - 10.1109/PDP.2016.107

DO - 10.1109/PDP.2016.107

M3 - Conference contribution

SN - 978-1-4673-8775-0

SP - 495

EP - 503

BT - Proceedings of the 24th Euromicro International Conference on Parallel, Distributed, and Network-Based Processing (PDP 2016)

PB - IEEE Computer Society

CY - USA

ER -

Amighi A, Blom S, Huisman M. VerCors: A Layered Approach to Practical Verification of Concurrent Software. In Proceedings of the 24th Euromicro International Conference on Parallel, Distributed, and Network-Based Processing (PDP 2016). USA: IEEE Computer Society. 2016. p. 495-503. Available from, DOI: 10.1109/PDP.2016.107