Reference

Reference specification

This module describes a set of memory events ordered by local time. It provides actions that assign global time to events in increasing order. The pre-conditions of these actions enforce the consistency model (that is, what orderings in local time must be preserved in global time).

include order

module sht_reference(id,key,data) = {

type of local time

    ghost type ltime
    instance props : totally_ordered(ltime)

type of hash table ops

    type otype = {read, write}

structure of hash table events to serialize

    module hashev = {
    individual type_ : otype
    individual key_ : key.t
    individual data_  : data # data for write and cas
    individual id_ : id      # process id of op
    relation serialized      # this event has happened

    init ~serialized
    }

memory events by local time

    instantiate evs(T:ltime) : hashev

global memory state obeys partial function axiom

    individual hash(A:key.t) : data

An aribtrary init value

    init hash(A) = 0

serialize an event lt at current global time. The "id" parameter tells us what process is serializing the event.

    action serialize(lt:ltime, id_:id) = {

    assert ~evs(lt).serialized;

serialize at current global time

    evs(lt).serialized := true;

update the global memory state

    local a : key.t, d : data {
            a := evs(lt).key_;
        d := evs(lt).data_;
        if evs(lt).type_ = read {
        evs(lt).data_ := hash(a)
        }
        else { # write
        hash(a) := d
        }
    }
    }
    delegate serialize


    relation generated(T:ltime)
    init ~generated(T)

begin transaction

    action begin(id_:id,op:otype,key_:key.t,data_:data) returns (lt:ltime) = {
    assume exists T. ~generated(T);
    if some c:ltime. ~generated(c) minimizing c {
        evs(c).type_ := op;
        evs(c).key_ := key_;
        evs(c).data_  := data_;
        evs(c).id_ := id_;
        generated(c) := true;
        lt := c
    }
    }

end transaction

    action end(lt:ltime) = {
    assert evs(lt).serialized
    }
    delegate end

    object impl = {
    interpret ltime -> int
    }

    isolate iso_props = props with impl
}