A thread-safe Term Library: (with a new fast mutual exclusion protocol)

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

A thread-safe Term Library: (with a new fast mutual exclusion protocol)

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

Onderzoeksoutput: Bijdrage aan tijdschrift › Tijdschriftartikel › Academic

Samenvatting

Terms are one of the fundamental data structures for computing. E.g. every expression characterisable by a context free grammar is a term. Remarkably, terms are not yet standard in common programming languages although term libraries have already been proposed in the 1990-ies. 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 library. Benchmarks show this Term Library to scale well, and to compare favourably with sequential versions. Using the new library in an existing state space generation tool, very substantial speed ups can be obtained.

Originele taal-2	Engels
Aantal pagina's	13
Tijdschrift	CoRR
Volume	abs/2111.02706
Status	Gepubliceerd - 4 nov. 2021

Bibliografische nota

DBLP License: DBLP's bibliographic metadata records provided through http://dblp.org/ are distributed under a Creative Commons CC0 1.0 Universal Public Domain Dedication. Although the bibliographic metadata records are provided consistent with CC0 1.0 Dedication, the content described by the metadata records is not. Content may be subject to copyright, rights of privacy, rights of publicity and other restrictions.

Toegang tot document

https://arxiv.org/abs/2111.02706

Citeer dit

@article{d182b999a1b54f1a8c1f63b016e52f10,

title = "A thread-safe Term Library: (with a new fast mutual exclusion protocol)",

abstract = "Terms are one of the fundamental data structures for computing. E.g. every expression characterisable by a context free grammar is a term. Remarkably, terms are not yet standard in common programming languages although term libraries have already been proposed in the 1990-ies. 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 library. Benchmarks show this Term Library to scale well, and to compare favourably with sequential versions. Using the new library in an existing state space generation tool, very substantial speed ups can be obtained. ",

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

note = "DBLP License: DBLP's bibliographic metadata records provided through http://dblp.org/ are distributed under a Creative Commons CC0 1.0 Universal Public Domain Dedication. Although the bibliographic metadata records are provided consistent with CC0 1.0 Dedication, the content described by the metadata records is not. Content may be subject to copyright, rights of privacy, rights of publicity and other restrictions.",

year = "2021",

month = nov,

day = "4",

language = "English",

volume = "abs/2111.02706",

journal = "CoRR",

issn = "2331-8422",

publisher = "Schloss Dagstuhl - Leibniz-Zentrum f{\"u}r Informatik",

}

TY - JOUR

T1 - A thread-safe Term Library

T2 - (with a new fast mutual exclusion protocol)

AU - Groote, Jan Friso

AU - Laveaux, Maurice

AU - Spaendonck, P. H. M. van

N1 - DBLP License: DBLP's bibliographic metadata records provided through http://dblp.org/ are distributed under a Creative Commons CC0 1.0 Universal Public Domain Dedication. Although the bibliographic metadata records are provided consistent with CC0 1.0 Dedication, the content described by the metadata records is not. Content may be subject to copyright, rights of privacy, rights of publicity and other restrictions.

PY - 2021/11/4

Y1 - 2021/11/4

N2 - Terms are one of the fundamental data structures for computing. E.g. every expression characterisable by a context free grammar is a term. Remarkably, terms are not yet standard in common programming languages although term libraries have already been proposed in the 1990-ies. 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 library. Benchmarks show this Term Library to scale well, and to compare favourably with sequential versions. 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 data structures for computing. E.g. every expression characterisable by a context free grammar is a term. Remarkably, terms are not yet standard in common programming languages although term libraries have already been proposed in the 1990-ies. 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 library. Benchmarks show this Term Library to scale well, and to compare favourably with sequential versions. Using the new library in an existing state space generation tool, very substantial speed ups can be obtained.

M3 - Article

SN - 2331-8422

VL - abs/2111.02706

JO - CoRR

JF - CoRR

ER -

A thread-safe Term Library: (with a new fast mutual exclusion protocol)

Samenvatting

Bibliografische nota

Toegang tot document

Vingerafdruk

Citeer dit