Shards

A shard is a concrete representation of the values of a range of keys [lo,hi) in the directory. The protocol uses shards to send directory data between servers. Shards have to be a POD datatype because we send them over the network. Shards are encoded so that if a key does not occur in the array, then its value is implicitly the background value 0. This means the interval [lo,hi) can be much larger than the number of keys actually represented in the shard.

We implement a shard as a struct containing the bounds lo and hi, represented by key iterators, and an array of key/value pair that maps each key in the range [lo,hi) that is present in the hash table to its value.

To represent the key/value array, we use the keyvalue module from the standard library. The specification of keyvalue provides a relation key_at(A,I,K) indicating that in array A, index I contains key K. There is also a function value_at(A,I) that yields the value at index I. Specifying the keys with a relation rather than a function is very helpful in this application, because it let’s use write a property like “every key K with property p is present in the array” without creating a function cycle. It’s worth having a look at the module keyval in collections.ivy, since it uses a very typical approach to specifying a containter type.

Meanwhile, here is the definition of shards:

include order
include collections

module table_shard(key,data) = {

    instance index : unbounded_sequence
    instance kvt : keyval(index,key.t,data)

    type t = struct {
        lo : key.iter.t,
        hi : key.iter.t,
        kv : kvt.t
    }

    relation key_at(S:t,I:index.t,X:key.t) = kv(S).key_at(I,X)
    function value_at(S:t,I:index.t) = kv(S).value_at(I)

    function value(S:t,X:key.t) = some Y. key_at(S,Y,X) in value_at(S,Y) else 0
    function valid(s:t) = forall X,Y,Z. key_at(s,Y,X) & key_at(s,Z,X) -> Y = Z

}

For convenience, we define key_at and value_at as shorthands for the corresponding members of keyval.

The representation function value returns some data associated with a key if the key occurs anywhere in the shard, otherwise it returns the background value 0. This gives the key/value map associated with the shard. The some quantifier in the definition of value introduces an implicit function from keys to their positions in the array. This is not a problem, however, since there is no function in the interface from positions back to keys.

The valid predicate tells us that a given key does not accur twice in the array. In particular, in a valid shard, the value function is uniquely defined. The predicate valid is an object invariant that users of table_shard will have to carry around.