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

Research output: Contribution to journal › Article › Academic

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.

Original language	English
Number of pages	13
Journal	CoRR
Volume	abs/2111.02706
Publication status	Published - 4 Nov 2021

Bibliographical 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.

Access to Document

https://arxiv.org/abs/2111.02706

Cite this

@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)

Abstract

Bibliographical note

Access to Document

Fingerprint

Cite this