Verifying atomicity preservation and deadlock freedom of a generic shared variable mechanism used in model-to-code transformations

D. Zhang; D. Bošnački; M.G.J. van den Brand; C. Huizing; B. Jacobs; R. Kuiper; A. Wijs

doi:10.1007/978-3-319-66302-9_13

Verifying atomicity preservation and deadlock freedom of a generic shared variable mechanism used in model-to-code transformations

D. Zhang, D. Bošnački, M.G.J. van den Brand, C. Huizing, B. Jacobs, R. Kuiper, A. Wijs

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

6 Citations (Scopus)

2 Downloads (Pure)

Abstract

A challenging aspect of model-to-code transformations is to ensure that the semantic behavior of the input model is preserved in the output code. When constructing concurrent systems, this is mainly difficult due to the non-deterministic potential interaction between threads. In this paper, we consider this issue for a framework that implements a transformation chain from models expressed in the state machine based domain specific language SLCO to Java. In particular, we provide a fine-grained generic mechanism to preserve atomicity of SLCO statements in the Java implementation. We give its generic specification based on separation logic and verify it using the verification tool VeriFast. The solution can be regarded as a reusable module to safely implement atomic operations in concurrent systems. Moreover, we also prove with VeriFast that our mechanism does not introduce deadlocks. The specification formally ensures that the locks are not reentrant which simplifies the formal treatment of the Java locks.

Original language	English
Title of host publication	Model-Driven Engineering and Software Development - 4th International Conference, MODELSWARD 2016, Revised Selected Papers
Editors	S. Hammoudi, L.F. Pires, B. Selic, P. Desfray
Publisher	Springer
Pages	249-273
Number of pages	25
ISBN (Electronic)	978-3-319-66302-9
ISBN (Print)	978-3-319-66301-2
DOIs	https://doi.org/10.1007/978-3-319-66302-9_13
Publication status	Published - 2017
Event	4th International Conference on Model-Driven Engineering and Software Development (MODELSWARD 2016), February 19-21, 2016, Rome, Italy: Doctoral Consortium, 20 February 2016 - Rome, Italy Duration: 19 Feb 2016 → 21 Feb 2016

Publication series

Name	Communications in Computer and Information Science
Volume	692
ISSN (Print)	1865-0929

Conference

Conference	4th International Conference on Model-Driven Engineering and Software Development (MODELSWARD 2016), February 19-21, 2016, Rome, Italy
Country/Territory	Italy
City	Rome
Period	19/02/16 → 21/02/16

Keywords

Atomicity
Code generation
Concurrency
Deadlock freedom
Formal verification
Model transformation
Separation logic

Access to Document

10.1007/978-3-319-66302-9_13

Cite this

Zhang, D., Bošnački, D., van den Brand, M. G. J., Huizing, C., Jacobs, B., Kuiper, R., & Wijs, A. (2017). Verifying atomicity preservation and deadlock freedom of a generic shared variable mechanism used in model-to-code transformations. In S. Hammoudi, L. F. Pires, B. Selic, & P. Desfray (Eds.), Model-Driven Engineering and Software Development - 4th International Conference, MODELSWARD 2016, Revised Selected Papers (pp. 249-273). (Communications in Computer and Information Science; Vol. 692). Springer. https://doi.org/10.1007/978-3-319-66302-9_13

Zhang, D. ; Bošnački, D. ; van den Brand, M.G.J. et al. / Verifying atomicity preservation and deadlock freedom of a generic shared variable mechanism used in model-to-code transformations. Model-Driven Engineering and Software Development - 4th International Conference, MODELSWARD 2016, Revised Selected Papers. editor / S. Hammoudi ; L.F. Pires ; B. Selic ; P. Desfray. Springer, 2017. pp. 249-273 (Communications in Computer and Information Science).

@inproceedings{713da09f0add413db2da93ddcd66c2c7,

title = "Verifying atomicity preservation and deadlock freedom of a generic shared variable mechanism used in model-to-code transformations",

abstract = "A challenging aspect of model-to-code transformations is to ensure that the semantic behavior of the input model is preserved in the output code. When constructing concurrent systems, this is mainly difficult due to the non-deterministic potential interaction between threads. In this paper, we consider this issue for a framework that implements a transformation chain from models expressed in the state machine based domain specific language SLCO to Java. In particular, we provide a fine-grained generic mechanism to preserve atomicity of SLCO statements in the Java implementation. We give its generic specification based on separation logic and verify it using the verification tool VeriFast. The solution can be regarded as a reusable module to safely implement atomic operations in concurrent systems. Moreover, we also prove with VeriFast that our mechanism does not introduce deadlocks. The specification formally ensures that the locks are not reentrant which simplifies the formal treatment of the Java locks.",

keywords = "Atomicity, Code generation, Concurrency, Deadlock freedom, Formal verification, Model transformation, Separation logic",

author = "D. Zhang and D. Bo{\v s}na{\v c}ki and {van den Brand}, M.G.J. and C. Huizing and B. Jacobs and R. Kuiper and A. Wijs",

year = "2017",

doi = "10.1007/978-3-319-66302-9_13",

language = "English",

isbn = "978-3-319-66301-2",

series = "Communications in Computer and Information Science",

publisher = "Springer",

pages = "249--273",

editor = "S. Hammoudi and L.F. Pires and B. Selic and P. Desfray",

booktitle = "Model-Driven Engineering and Software Development - 4th International Conference, MODELSWARD 2016, Revised Selected Papers",

address = "Germany",

note = "4th International Conference on Model-Driven Engineering and Software Development (MODELSWARD 2016), February 19-21, 2016, Rome, Italy : Doctoral Consortium, 20 February 2016 ; Conference date: 19-02-2016 Through 21-02-2016",

}

Zhang, D, Bošnački, D , van den Brand, MGJ , Huizing, C, Jacobs, B, Kuiper, R & Wijs, A 2017, Verifying atomicity preservation and deadlock freedom of a generic shared variable mechanism used in model-to-code transformations. in S Hammoudi, LF Pires, B Selic & P Desfray (eds), Model-Driven Engineering and Software Development - 4th International Conference, MODELSWARD 2016, Revised Selected Papers. Communications in Computer and Information Science, vol. 692, Springer, pp. 249-273, 4th International Conference on Model-Driven Engineering and Software Development (MODELSWARD 2016), February 19-21, 2016, Rome, Italy, Rome, Italy, 19/02/16. https://doi.org/10.1007/978-3-319-66302-9_13

Verifying atomicity preservation and deadlock freedom of a generic shared variable mechanism used in model-to-code transformations. / Zhang, D.; Bošnački, D.; van den Brand, M.G.J. et al.
Model-Driven Engineering and Software Development - 4th International Conference, MODELSWARD 2016, Revised Selected Papers. ed. / S. Hammoudi; L.F. Pires; B. Selic; P. Desfray. Springer, 2017. p. 249-273 (Communications in Computer and Information Science; Vol. 692).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Verifying atomicity preservation and deadlock freedom of a generic shared variable mechanism used in model-to-code transformations

AU - Zhang, D.

AU - Bošnački, D.

AU - van den Brand, M.G.J.

AU - Huizing, C.

AU - Jacobs, B.

AU - Kuiper, R.

AU - Wijs, A.

PY - 2017

Y1 - 2017

N2 - A challenging aspect of model-to-code transformations is to ensure that the semantic behavior of the input model is preserved in the output code. When constructing concurrent systems, this is mainly difficult due to the non-deterministic potential interaction between threads. In this paper, we consider this issue for a framework that implements a transformation chain from models expressed in the state machine based domain specific language SLCO to Java. In particular, we provide a fine-grained generic mechanism to preserve atomicity of SLCO statements in the Java implementation. We give its generic specification based on separation logic and verify it using the verification tool VeriFast. The solution can be regarded as a reusable module to safely implement atomic operations in concurrent systems. Moreover, we also prove with VeriFast that our mechanism does not introduce deadlocks. The specification formally ensures that the locks are not reentrant which simplifies the formal treatment of the Java locks.

AB - A challenging aspect of model-to-code transformations is to ensure that the semantic behavior of the input model is preserved in the output code. When constructing concurrent systems, this is mainly difficult due to the non-deterministic potential interaction between threads. In this paper, we consider this issue for a framework that implements a transformation chain from models expressed in the state machine based domain specific language SLCO to Java. In particular, we provide a fine-grained generic mechanism to preserve atomicity of SLCO statements in the Java implementation. We give its generic specification based on separation logic and verify it using the verification tool VeriFast. The solution can be regarded as a reusable module to safely implement atomic operations in concurrent systems. Moreover, we also prove with VeriFast that our mechanism does not introduce deadlocks. The specification formally ensures that the locks are not reentrant which simplifies the formal treatment of the Java locks.

KW - Atomicity

KW - Code generation

KW - Concurrency

KW - Deadlock freedom

KW - Formal verification

KW - Model transformation

KW - Separation logic

UR - http://www.scopus.com/inward/record.url?scp=85030115904&partnerID=8YFLogxK

U2 - 10.1007/978-3-319-66302-9_13

DO - 10.1007/978-3-319-66302-9_13

M3 - Conference contribution

AN - SCOPUS:85030115904

SN - 978-3-319-66301-2

T3 - Communications in Computer and Information Science

SP - 249

EP - 273

BT - Model-Driven Engineering and Software Development - 4th International Conference, MODELSWARD 2016, Revised Selected Papers

A2 - Hammoudi, S.

A2 - Pires, L.F.

A2 - Selic, B.

A2 - Desfray, P.

PB - Springer

T2 - 4th International Conference on Model-Driven Engineering and Software Development (MODELSWARD 2016), February 19-21, 2016, Rome, Italy

Y2 - 19 February 2016 through 21 February 2016

ER -

Zhang D, Bošnački D , van den Brand MGJ , Huizing C, Jacobs B, Kuiper R et al. Verifying atomicity preservation and deadlock freedom of a generic shared variable mechanism used in model-to-code transformations. In Hammoudi S, Pires LF, Selic B, Desfray P, editors, Model-Driven Engineering and Software Development - 4th International Conference, MODELSWARD 2016, Revised Selected Papers. Springer. 2017. p. 249-273. (Communications in Computer and Information Science). doi: 10.1007/978-3-319-66302-9_13

Verifying atomicity preservation and deadlock freedom of a generic shared variable mechanism used in model-to-code transformations

Abstract

Publication series

Conference

Keywords

Access to Document

Other files and links

Fingerprint

Cite this