WAIT-FREE LINEARIZATION WITH A MECHANICAL PROOF

Wim H. Hesselink

WAIT-FREE LINEARIZATION WITH A MECHANICAL PROOF

Wim H. Hesselink

Fundamental Computing

Research output: Contribution to journal › Article › Academic › peer-review

6 Citations (Scopus)

428 Downloads (Pure)

Abstract

The correctness of a program for wait-free linearization of an arbitrary shared data object in bounded memory is verified mechanically. The program uses atomic read-write registers, an array of consensus registers and one compare and swap register. In the program, a number of processes concurrently inspect and modify a pointer structure without waiting. Consequently, the proof of correctness is very delicate. The theorem prover NQTHM of Boyer and Moore has been used to mechanically certify the correctness.

Original language	English
Pages (from-to)	21-36
Number of pages	16
Journal	Distributed computing
Volume	9
Issue number	1
Publication status	Published - Aug-1995

Keywords

LINEARIZABLE
SHARED DATA OBJECT
CONSENSUS
WAIT-FREE
MEMORY MANAGEMENT
CORRECTNESS
INVARIANT
GRAIN OF ATOMICITY
MECHANICAL VERIFICATION
BOYER MOORE LOGIC
OBJECTS
SYSTEMS

Access to Document

1995DistrCompHesselink.pdfFinal publisher's version, 1.68 MB

Handle.net

Persistent link

Cite this

@article{890babfc9790479997d83587c9a9d589,

title = "WAIT-FREE LINEARIZATION WITH A MECHANICAL PROOF",

abstract = "The correctness of a program for wait-free linearization of an arbitrary shared data object in bounded memory is verified mechanically. The program uses atomic read-write registers, an array of consensus registers and one compare and swap register. In the program, a number of processes concurrently inspect and modify a pointer structure without waiting. Consequently, the proof of correctness is very delicate. The theorem prover NQTHM of Boyer and Moore has been used to mechanically certify the correctness.",

keywords = "LINEARIZABLE, SHARED DATA OBJECT, CONSENSUS, WAIT-FREE, MEMORY MANAGEMENT, CORRECTNESS, INVARIANT, GRAIN OF ATOMICITY, MECHANICAL VERIFICATION, BOYER MOORE LOGIC, OBJECTS, SYSTEMS",

author = "Hesselink, {Wim H.}",

note = "Relation: http://www.rug.nl/informatica/organisatie/overorganisatie/iwi Rights: University of Groningen. Research Institute for Mathematics and Computing Science (IWI)",

year = "1995",

month = aug,

language = "English",

volume = "9",

pages = "21--36",

journal = "Distributed computing",

issn = "0178-2770",

number = "1",

}

TY - JOUR

T1 - WAIT-FREE LINEARIZATION WITH A MECHANICAL PROOF

AU - Hesselink, Wim H.

N1 - Relation: http://www.rug.nl/informatica/organisatie/overorganisatie/iwi Rights: University of Groningen. Research Institute for Mathematics and Computing Science (IWI)

PY - 1995/8

Y1 - 1995/8

N2 - The correctness of a program for wait-free linearization of an arbitrary shared data object in bounded memory is verified mechanically. The program uses atomic read-write registers, an array of consensus registers and one compare and swap register. In the program, a number of processes concurrently inspect and modify a pointer structure without waiting. Consequently, the proof of correctness is very delicate. The theorem prover NQTHM of Boyer and Moore has been used to mechanically certify the correctness.

AB - The correctness of a program for wait-free linearization of an arbitrary shared data object in bounded memory is verified mechanically. The program uses atomic read-write registers, an array of consensus registers and one compare and swap register. In the program, a number of processes concurrently inspect and modify a pointer structure without waiting. Consequently, the proof of correctness is very delicate. The theorem prover NQTHM of Boyer and Moore has been used to mechanically certify the correctness.

KW - LINEARIZABLE

KW - SHARED DATA OBJECT

KW - CONSENSUS

KW - WAIT-FREE

KW - MEMORY MANAGEMENT

KW - CORRECTNESS

KW - INVARIANT

KW - GRAIN OF ATOMICITY

KW - MECHANICAL VERIFICATION

KW - BOYER MOORE LOGIC

KW - OBJECTS

KW - SYSTEMS

M3 - Article

SN - 0178-2770

VL - 9

SP - 21

EP - 36

JO - Distributed computing

JF - Distributed computing

IS - 1

ER -

WAIT-FREE LINEARIZATION WITH A MECHANICAL PROOF

Abstract

Keywords

Access to Document

Handle.net

Fingerprint

Cite this