A Thread-Safe Term Library: (with a New Fast Mutual Exclusion Protocol)

Jan Friso Groote; Maurice Laveaux; P. H.M. van Spaendonck

doi:10.1007/978-3-031-19849-6_25

A Thread-Safe Term Library: (with a New Fast Mutual Exclusion Protocol)

Jan Friso Groote, Maurice Laveaux, P. H.M. van Spaendonck

Onderzoeksoutput: Hoofdstuk in Boek/Rapport/Congresprocedure › Conferentiebijdrage › Academic › peer review

2 Citaten (Scopus)

Samenvatting

Terms are one of the fundamental mathematical concepts in computing. E.g. every expression characterisable by a context free grammar is a term. We developed a thread-safe Term Library. The biggest challenge is to implement hyper-efficient multi-reader/single-writer mutual exclusion for which we designed the new busy-forbidden protocol. Model checking is used to show both the correctness of the protocol and the Term Library. Benchmarks show this Term Library has little overhead compared to sequential versions and outperforms them already on two processors. Using the new library in an existing state space generation tool, very substantial speed ups can be obtained.

Originele taal-2	Engels
Titel	Leveraging Applications of Formal Methods, Verification and Validation. Verification Principles - 11th International Symposium, ISoLA 2022, Proceedings
Redacteuren	Tiziana Margaria, Bernhard Steffen
Uitgeverij	Springer
Pagina's	422-459
Aantal pagina's	38
ISBN van geprinte versie	9783031198489
DOI's	https://doi.org/10.1007/978-3-031-19849-6_25
Status	Gepubliceerd - 2022
Evenement	11th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2022 - Rhodes, Griekenland Duur: 22 okt. 2022 → 30 okt. 2022

Publicatie series

Naam	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	13701 LNCS
ISSN van geprinte versie	0302-9743
ISSN van elektronische versie	1611-3349

Congres

Congres	11th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2022
Land/Regio	Griekenland
Stad	Rhodes
Periode	22/10/22 → 30/10/22

Bibliografische nota

Publisher Copyright:
© 2022, The Author(s), under exclusive license to Springer Nature Switzerland AG.

Toegang tot document

10.1007/978-3-031-19849-6_25

Andere bestanden en links

Link naar publicatie in Scopus

Citeer dit

Groote, J. F., Laveaux, M., & van Spaendonck, P. H. M. (2022). A Thread-Safe Term Library: (with a New Fast Mutual Exclusion Protocol). In T. Margaria, & B. Steffen (editors), Leveraging Applications of Formal Methods, Verification and Validation. Verification Principles - 11th International Symposium, ISoLA 2022, Proceedings (blz. 422-459). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 13701 LNCS). Springer. https://doi.org/10.1007/978-3-031-19849-6_25

Groote, Jan Friso ; Laveaux, Maurice ; van Spaendonck, P. H.M. / A Thread-Safe Term Library : (with a New Fast Mutual Exclusion Protocol). Leveraging Applications of Formal Methods, Verification and Validation. Verification Principles - 11th International Symposium, ISoLA 2022, Proceedings. redacteur / Tiziana Margaria ; Bernhard Steffen. Springer, 2022. blz. 422-459 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{ea05153d1c8042cb8928ff97f110e98c,

title = "A Thread-Safe Term Library: (with a New Fast Mutual Exclusion Protocol)",

abstract = "Terms are one of the fundamental mathematical concepts in computing. E.g. every expression characterisable by a context free grammar is a term. We developed a thread-safe Term Library. The biggest challenge is to implement hyper-efficient multi-reader/single-writer mutual exclusion for which we designed the new busy-forbidden protocol. Model checking is used to show both the correctness of the protocol and the Term Library. Benchmarks show this Term Library has little overhead compared to sequential versions and outperforms them already on two processors. Using the new library in an existing state space generation tool, very substantial speed ups can be obtained.",

keywords = "Model checking, Mutual exclusion, Term library, Thread-safe",

author = "Groote, {Jan Friso} and Maurice Laveaux and {van Spaendonck}, {P. H.M.}",

note = "Funding Information: Supported by projects 612.001.751 (NWO, AVVA) and 00795160 (TTW, MASCOT). Publisher Copyright: {\textcopyright} 2022, The Author(s), under exclusive license to Springer Nature Switzerland AG.; 11th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2022 ; Conference date: 22-10-2022 Through 30-10-2022",

year = "2022",

doi = "10.1007/978-3-031-19849-6_25",

language = "English",

isbn = "9783031198489",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer",

pages = "422--459",

editor = "Tiziana Margaria and Bernhard Steffen",

booktitle = "Leveraging Applications of Formal Methods, Verification and Validation. Verification Principles - 11th International Symposium, ISoLA 2022, Proceedings",

address = "Germany",

}

Groote, JF , Laveaux, M & van Spaendonck, PHM 2022, A Thread-Safe Term Library: (with a New Fast Mutual Exclusion Protocol). in T Margaria & B Steffen (uitgave), Leveraging Applications of Formal Methods, Verification and Validation. Verification Principles - 11th International Symposium, ISoLA 2022, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 13701 LNCS, Springer, blz. 422-459, 11th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2022, Rhodes, Griekenland, 22/10/22. https://doi.org/10.1007/978-3-031-19849-6_25

A Thread-Safe Term Library: (with a New Fast Mutual Exclusion Protocol). / Groote, Jan Friso ; Laveaux, Maurice ; van Spaendonck, P. H.M.
Leveraging Applications of Formal Methods, Verification and Validation. Verification Principles - 11th International Symposium, ISoLA 2022, Proceedings. uitgave / Tiziana Margaria; Bernhard Steffen. Springer, 2022. blz. 422-459 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 13701 LNCS).

Onderzoeksoutput: Hoofdstuk in Boek/Rapport/Congresprocedure › Conferentiebijdrage › Academic › peer review

TY - GEN

T1 - A Thread-Safe Term Library

T2 - 11th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2022

AU - Groote, Jan Friso

AU - Laveaux, Maurice

AU - van Spaendonck, P. H.M.

N1 - Funding Information: Supported by projects 612.001.751 (NWO, AVVA) and 00795160 (TTW, MASCOT). Publisher Copyright: © 2022, The Author(s), under exclusive license to Springer Nature Switzerland AG.

PY - 2022

Y1 - 2022

N2 - Terms are one of the fundamental mathematical concepts in computing. E.g. every expression characterisable by a context free grammar is a term. We developed a thread-safe Term Library. The biggest challenge is to implement hyper-efficient multi-reader/single-writer mutual exclusion for which we designed the new busy-forbidden protocol. Model checking is used to show both the correctness of the protocol and the Term Library. Benchmarks show this Term Library has little overhead compared to sequential versions and outperforms them already on two processors. Using the new library in an existing state space generation tool, very substantial speed ups can be obtained.

AB - Terms are one of the fundamental mathematical concepts in computing. E.g. every expression characterisable by a context free grammar is a term. We developed a thread-safe Term Library. The biggest challenge is to implement hyper-efficient multi-reader/single-writer mutual exclusion for which we designed the new busy-forbidden protocol. Model checking is used to show both the correctness of the protocol and the Term Library. Benchmarks show this Term Library has little overhead compared to sequential versions and outperforms them already on two processors. Using the new library in an existing state space generation tool, very substantial speed ups can be obtained.

KW - Model checking

KW - Mutual exclusion

KW - Term library

KW - Thread-safe

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

U2 - 10.1007/978-3-031-19849-6_25

DO - 10.1007/978-3-031-19849-6_25

M3 - Conference contribution

AN - SCOPUS:85142747990

SN - 9783031198489

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 422

EP - 459

BT - Leveraging Applications of Formal Methods, Verification and Validation. Verification Principles - 11th International Symposium, ISoLA 2022, Proceedings

A2 - Margaria, Tiziana

A2 - Steffen, Bernhard

PB - Springer

Y2 - 22 October 2022 through 30 October 2022

ER -

Groote JF , Laveaux M , van Spaendonck PHM. A Thread-Safe Term Library: (with a New Fast Mutual Exclusion Protocol). In Margaria T, Steffen B, redacteurs, Leveraging Applications of Formal Methods, Verification and Validation. Verification Principles - 11th International Symposium, ISoLA 2022, Proceedings. Springer. 2022. blz. 422-459. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-031-19849-6_25

A Thread-Safe Term Library: (with a New Fast Mutual Exclusion Protocol)

Samenvatting

Publicatie series

Congres

Bibliografische nota

Toegang tot document

Andere bestanden en links

Vingerafdruk

Citeer dit