Resource protection using atomics: patterns and verifications

A. Amighi, Stefan Blom, Marieke Huisman

Research output: Book/ReportReportProfessional

28 Downloads (Pure)

Abstract

Modular reasoning about non-blocking concurrent data structures is crucial to establish the correctness of concurrent applications. To achieve this, specifications of the synchronization mechanisms used by these non-blocking concurrent classes to prevent concurrent access to shared data, are essential. This paper presents an approach to specifying such lock-free synchronization mechanisms in terms of the thread's role and permissions. The approach is formalized in a specification for the AtomicInteger class from the java.util.concurrent library, using abstract predicates and permission-based concurrent Separation Logic. The specification is set up to capture different synchronization patterns, both cooperative and competitive. We illustrate the use of the patterns in three case studies, where for each case study we verify that it indeed correctly synchronizes access to the protected data.
Original languageUndefined
Place of PublicationEnschede
PublisherCentre for Telematics and Information Technology (CTIT)
Number of pages14
Publication statusPublished - 1 May 2013

Publication series

NameCTIT Technical Report Series
PublisherUniversity of Twente, Centre for Telematica and Information Technology (CTIT)
No.TR-CTIT-13-10
ISSN (Print)1381-3625

Keywords

  • Permissions
  • Separation Logic
  • Verification
  • Java volatiles
  • Specification
  • Concurrency
  • IR-85886
  • METIS-296412
  • EWI-23306
  • atomics

Cite this

Amighi, A., Blom, S., & Huisman, M. (2013). Resource protection using atomics: patterns and verifications. (CTIT Technical Report Series; No. TR-CTIT-13-10). Enschede: Centre for Telematics and Information Technology (CTIT).
Amighi, A. ; Blom, Stefan ; Huisman, Marieke. / Resource protection using atomics: patterns and verifications. Enschede : Centre for Telematics and Information Technology (CTIT), 2013. 14 p. (CTIT Technical Report Series; TR-CTIT-13-10).
@book{04d6085a73554ef7bb7bcd564ac1e3b7,
title = "Resource protection using atomics: patterns and verifications",
abstract = "Modular reasoning about non-blocking concurrent data structures is crucial to establish the correctness of concurrent applications. To achieve this, specifications of the synchronization mechanisms used by these non-blocking concurrent classes to prevent concurrent access to shared data, are essential. This paper presents an approach to specifying such lock-free synchronization mechanisms in terms of the thread's role and permissions. The approach is formalized in a specification for the AtomicInteger class from the java.util.concurrent library, using abstract predicates and permission-based concurrent Separation Logic. The specification is set up to capture different synchronization patterns, both cooperative and competitive. We illustrate the use of the patterns in three case studies, where for each case study we verify that it indeed correctly synchronizes access to the protected data.",
keywords = "Permissions, Separation Logic, Verification, Java volatiles, Specification, Concurrency, IR-85886, METIS-296412, EWI-23306, atomics",
author = "A. Amighi and Stefan Blom and Marieke Huisman",
year = "2013",
month = "5",
day = "1",
language = "Undefined",
series = "CTIT Technical Report Series",
publisher = "Centre for Telematics and Information Technology (CTIT)",
number = "TR-CTIT-13-10",
address = "Netherlands",

}

Amighi, A, Blom, S & Huisman, M 2013, Resource protection using atomics: patterns and verifications. CTIT Technical Report Series, no. TR-CTIT-13-10, Centre for Telematics and Information Technology (CTIT), Enschede.

Resource protection using atomics: patterns and verifications. / Amighi, A.; Blom, Stefan; Huisman, Marieke.

Enschede : Centre for Telematics and Information Technology (CTIT), 2013. 14 p. (CTIT Technical Report Series; No. TR-CTIT-13-10).

Research output: Book/ReportReportProfessional

TY - BOOK

T1 - Resource protection using atomics: patterns and verifications

AU - Amighi, A.

AU - Blom, Stefan

AU - Huisman, Marieke

PY - 2013/5/1

Y1 - 2013/5/1

N2 - Modular reasoning about non-blocking concurrent data structures is crucial to establish the correctness of concurrent applications. To achieve this, specifications of the synchronization mechanisms used by these non-blocking concurrent classes to prevent concurrent access to shared data, are essential. This paper presents an approach to specifying such lock-free synchronization mechanisms in terms of the thread's role and permissions. The approach is formalized in a specification for the AtomicInteger class from the java.util.concurrent library, using abstract predicates and permission-based concurrent Separation Logic. The specification is set up to capture different synchronization patterns, both cooperative and competitive. We illustrate the use of the patterns in three case studies, where for each case study we verify that it indeed correctly synchronizes access to the protected data.

AB - Modular reasoning about non-blocking concurrent data structures is crucial to establish the correctness of concurrent applications. To achieve this, specifications of the synchronization mechanisms used by these non-blocking concurrent classes to prevent concurrent access to shared data, are essential. This paper presents an approach to specifying such lock-free synchronization mechanisms in terms of the thread's role and permissions. The approach is formalized in a specification for the AtomicInteger class from the java.util.concurrent library, using abstract predicates and permission-based concurrent Separation Logic. The specification is set up to capture different synchronization patterns, both cooperative and competitive. We illustrate the use of the patterns in three case studies, where for each case study we verify that it indeed correctly synchronizes access to the protected data.

KW - Permissions

KW - Separation Logic

KW - Verification

KW - Java volatiles

KW - Specification

KW - Concurrency

KW - IR-85886

KW - METIS-296412

KW - EWI-23306

KW - atomics

M3 - Report

T3 - CTIT Technical Report Series

BT - Resource protection using atomics: patterns and verifications

PB - Centre for Telematics and Information Technology (CTIT)

CY - Enschede

ER -

Amighi A, Blom S, Huisman M. Resource protection using atomics: patterns and verifications. Enschede: Centre for Telematics and Information Technology (CTIT), 2013. 14 p. (CTIT Technical Report Series; TR-CTIT-13-10).