Verifying linearizability via optimized refinement checking
Linearizability is an important correctness criterion for implementations of concurrent objects. Automatic checking of linearizability is challenging because it requires checking that: 1) All executions of concurrent operations are serializable, and 2) the serialized executions are correct with resp...
Saved in:
Main Authors: | , , , , , |
---|---|
Format: | text |
Language: | English |
Published: |
Institutional Knowledge at Singapore Management University
2013
|
Subjects: | |
Online Access: | https://ink.library.smu.edu.sg/sis_research/4996 https://ink.library.smu.edu.sg/context/sis_research/article/5999/viewcontent/10.1.1.385.4127.pdf |
Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
Institution: | Singapore Management University |
Language: | English |
id |
sg-smu-ink.sis_research-5999 |
---|---|
record_format |
dspace |
spelling |
sg-smu-ink.sis_research-59992020-03-12T09:40:40Z Verifying linearizability via optimized refinement checking LIU, Yang CHEN, Wei LIU, Yanhong A. SUN, Jun ZHANG, Shao Jie DONG, Jin Song Dong Linearizability is an important correctness criterion for implementations of concurrent objects. Automatic checking of linearizability is challenging because it requires checking that: 1) All executions of concurrent operations are serializable, and 2) the serialized executions are correct with respect to the sequential semantics. In this work, we describe a method to automatically check linearizability based on refinement relations from abstract specifications to concrete implementations. The method does not require that linearization points in the implementations be given, which is often difficult or impossible. However, the method takes advantage of linearization points if they are given. The method is based on refinement checking of finite-state systems specified as concurrent processes with shared variables. To tackle state space explosion, we develop and apply symmetry reduction, dynamic partial order reduction, and a combination of both for refinement checking. We have built the method into the PAT model checker, and used PAT to automatically check a variety of implementations of concurrent objects, including the first algorithm for scalable nonzero indicators. Our system is able to find all known and injected bugs in these implementations. 2013-01-07T08:00:00Z text application/pdf https://ink.library.smu.edu.sg/sis_research/4996 info:doi/10.1109/TSE.2012.82 https://ink.library.smu.edu.sg/context/sis_research/article/5999/viewcontent/10.1.1.385.4127.pdf http://creativecommons.org/licenses/by-nc-nd/4.0/ Research Collection School Of Computing and Information Systems eng Institutional Knowledge at Singapore Management University Linearizability refinement model checking PAT Programming Languages and Compilers Software Engineering |
institution |
Singapore Management University |
building |
SMU Libraries |
continent |
Asia |
country |
Singapore Singapore |
content_provider |
SMU Libraries |
collection |
InK@SMU |
language |
English |
topic |
Linearizability refinement model checking PAT Programming Languages and Compilers Software Engineering |
spellingShingle |
Linearizability refinement model checking PAT Programming Languages and Compilers Software Engineering LIU, Yang CHEN, Wei LIU, Yanhong A. SUN, Jun ZHANG, Shao Jie DONG, Jin Song Dong Verifying linearizability via optimized refinement checking |
description |
Linearizability is an important correctness criterion for implementations of concurrent objects. Automatic checking of linearizability is challenging because it requires checking that: 1) All executions of concurrent operations are serializable, and 2) the serialized executions are correct with respect to the sequential semantics. In this work, we describe a method to automatically check linearizability based on refinement relations from abstract specifications to concrete implementations. The method does not require that linearization points in the implementations be given, which is often difficult or impossible. However, the method takes advantage of linearization points if they are given. The method is based on refinement checking of finite-state systems specified as concurrent processes with shared variables. To tackle state space explosion, we develop and apply symmetry reduction, dynamic partial order reduction, and a combination of both for refinement checking. We have built the method into the PAT model checker, and used PAT to automatically check a variety of implementations of concurrent objects, including the first algorithm for scalable nonzero indicators. Our system is able to find all known and injected bugs in these implementations. |
format |
text |
author |
LIU, Yang CHEN, Wei LIU, Yanhong A. SUN, Jun ZHANG, Shao Jie DONG, Jin Song Dong |
author_facet |
LIU, Yang CHEN, Wei LIU, Yanhong A. SUN, Jun ZHANG, Shao Jie DONG, Jin Song Dong |
author_sort |
LIU, Yang |
title |
Verifying linearizability via optimized refinement checking |
title_short |
Verifying linearizability via optimized refinement checking |
title_full |
Verifying linearizability via optimized refinement checking |
title_fullStr |
Verifying linearizability via optimized refinement checking |
title_full_unstemmed |
Verifying linearizability via optimized refinement checking |
title_sort |
verifying linearizability via optimized refinement checking |
publisher |
Institutional Knowledge at Singapore Management University |
publishDate |
2013 |
url |
https://ink.library.smu.edu.sg/sis_research/4996 https://ink.library.smu.edu.sg/context/sis_research/article/5999/viewcontent/10.1.1.385.4127.pdf |
_version_ |
1770575186602491904 |