VerCors: A Layered Approach to Practical Verification of Concurrent Software

A. Amighi, Stefan Blom, Marieke Huisman

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

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. p. 495-503.

Research output: Scientific - peer-reviewConference contribution

@inbook{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",
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-19 February. 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: Scientific - peer-reviewConference contribution

TY - CHAP

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

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