Library of dSPIN models

  1. Concurrent B-tree interlocking protocol

    2. Source: "Concurrency of Operation on B-Trees", Acta Informatica, Vol. 9, 1977, Springer-Verlag, pp. 1-21.
    Description: A B-tree structure used in concurrent access by a number of updater processes. Each node of the tree has a lock channel used by updaters to synchronize. When accessing the tree, each updater holds the lock of the current node and of all its ancestors that are "unsafe" i.e., they might expand as consequence of the updator's action on the current node. When the structure reaches a maximum depth, every process stops.
    Properties: Scalable: in the number of updater processes (N), B-tree maximum depth (D) and B-tree order (K)
    Code: btree.prom
     
    N, K, D
    states
    transitions
    symmetry
    reductions
    garbage
    collection
    3, 2, 2
     28222
    36689
    no
    no
    3, 2, 2
    5812
    7726
    yes
    yes
    2, 2, 3
    171329
    197864
    no
    no
    2, 2, 3
    7203
    8687
    yes
    yes
    2, 4, 3
    > 2.01856e+06
    > 2.60416e+06
    no
    no
    2, 4, 3
    62868
    86768
    yes
    yes

     
  2. Concurrent ordered list

    3. Description: A simply linked list ordered by key nodes is accessed concurrently by an arbitrary number of updater processes. Every such process inserts arbitrary values in the list. An extra monitor (reader) process checks the list for integrity. Each node has a lock channel used by processes to synchronize. Each process needs to hold the lock of the current and next node in the list in order to preserve the structure. The number of insert actions done by each updater is bounded.
    Properties: Scalable: in the number of updater processes (N) and number of insert actions performed by each updater (MAX)
    Code:  ordlist.prom
     
    N, MAX
    states
    transitions
    symmetry
    reductions
    2, 3
    138094
    185281
    no
    2, 3
    28015
     37861
    yes
    2, 4
    1.35108e+06
    1.82266e+06
    no
    2, 4
    140265
     190741
    yes
    3, 2
    2.51513e+06
    3.54015e+06
    no
    3, 2
    256972
    369058
    yes