Long-lives Test-And-Set Using

Jaap-henk Hoepman

    Research output: Working paper

    6 Downloads (Pure)

    Abstract

    This paper studies the problem of implementing a shared memory test-and-set object using only shared registers. Our contribution is threefold. First, we present a general framework to allow reasoning about reusing one-shot shared memory objects in the construction of bounded space long-lived objects. Then we derive general theorems about test-and set objects that simplifies reasoning about their implementation. Finally we show the validity of our approach by constructing an n process long lived test-and-set object from n + 1 one-shot test-and-set objects, and proving this construction formally correct.
    Original languageEnglish
    Place of PublicationEnschede
    PublisherUniversity of Twente
    Number of pages19
    Publication statusPublished - 10 Sep 1999

    Fingerprint

    Data storage equipment

    Keywords

    • METIS-119091

    Cite this

    Hoepman, J. (1999). Long-lives Test-And-Set Using. Enschede: University of Twente.
    Hoepman, Jaap-henk. / Long-lives Test-And-Set Using. Enschede : University of Twente, 1999.
    @techreport{5025c57a3b4c413e8dc44e3eff72abb0,
    title = "Long-lives Test-And-Set Using",
    abstract = "This paper studies the problem of implementing a shared memory test-and-set object using only shared registers. Our contribution is threefold. First, we present a general framework to allow reasoning about reusing one-shot shared memory objects in the construction of bounded space long-lived objects. Then we derive general theorems about test-and set objects that simplifies reasoning about their implementation. Finally we show the validity of our approach by constructing an n process long lived test-and-set object from n + 1 one-shot test-and-set objects, and proving this construction formally correct.",
    keywords = "METIS-119091",
    author = "Jaap-henk Hoepman",
    year = "1999",
    month = "9",
    day = "10",
    language = "English",
    publisher = "University of Twente",
    address = "Netherlands",
    type = "WorkingPaper",
    institution = "University of Twente",

    }

    Hoepman, J 1999 'Long-lives Test-And-Set Using' University of Twente, Enschede.

    Long-lives Test-And-Set Using. / Hoepman, Jaap-henk.

    Enschede : University of Twente, 1999.

    Research output: Working paper

    TY - UNPB

    T1 - Long-lives Test-And-Set Using

    AU - Hoepman, Jaap-henk

    PY - 1999/9/10

    Y1 - 1999/9/10

    N2 - This paper studies the problem of implementing a shared memory test-and-set object using only shared registers. Our contribution is threefold. First, we present a general framework to allow reasoning about reusing one-shot shared memory objects in the construction of bounded space long-lived objects. Then we derive general theorems about test-and set objects that simplifies reasoning about their implementation. Finally we show the validity of our approach by constructing an n process long lived test-and-set object from n + 1 one-shot test-and-set objects, and proving this construction formally correct.

    AB - This paper studies the problem of implementing a shared memory test-and-set object using only shared registers. Our contribution is threefold. First, we present a general framework to allow reasoning about reusing one-shot shared memory objects in the construction of bounded space long-lived objects. Then we derive general theorems about test-and set objects that simplifies reasoning about their implementation. Finally we show the validity of our approach by constructing an n process long lived test-and-set object from n + 1 one-shot test-and-set objects, and proving this construction formally correct.

    KW - METIS-119091

    M3 - Working paper

    BT - Long-lives Test-And-Set Using

    PB - University of Twente

    CY - Enschede

    ER -

    Hoepman J. Long-lives Test-And-Set Using. Enschede: University of Twente. 1999 Sep 10.