flat.md 3.71 KB
Newer Older
Zhen Zhang's avatar
Zhen Zhang committed
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
Flat combiner
=====

The flat combiner proofs is based on three major components:

1. Extensive use of *evidence map*, a general implementation of a heap-like structure
2. treiber's stack with per-item invariants
3. helping protocols encoded by exclusive monoids

## Evidence map

The idea is to simulate the heap we already have -- but generalize `loc` as `K` and `val` as `V`. So we can break down the fragmental ownerships, establish agreement over the `K`'s value etc. It is called that way because its generality and a definition called `ev`, which existentially equalifies over the fraction thus serves as kind of a duplicable evidence of existence of some agreed value pointed by certain key.

Concretely:

$$EvMap(K, V) = AUTH(FINMAP(K, FRAC \times AG(V)))$$

$$ev_\gamma(k, v) = \exists q, own_\gamma(\circ \{ k \mapsto (q, Agree(v))\})$$

## Treiber's stack

This stack contains all the "slots" that are used as a location pointing to request/response.

The stack has two layer of specification: The first layer is logically atomic triple style spec, containing `push`, and `pop`. The second layer is built on top of first layer, featuring a global, per-item invariant; it has `push`, and `iter`.

It is also built with the evidence map.

So here is the point:

1. `iter` doesn't have an atomic spec because the implementation just traverses along the link and doesn't enforce any atomicity, for example, guaranteeing that the traversed nodes will stay the same etc.
2. `pop` doesn't have an invariant spec because the invariant is based the model of immutable sharing, thus we can only *know* that some `R` holds for certain element, but we can't get this `R` into local state (since we can't shrink the `evmap` simply by giving an `ev`).

Here are the specs:

### constructor

$$\{ \top \} new\_stack \{s, is\_stack(s) \}$$

### atomic ones

push

$$\langle xs, hd. s \mapsto \#hd* is\_list(hd, xs) \rangle \\
  push(\#s, x) \\
  \langle ret. ret = \#() \land \exists hd', s \mapsto \#hd'* hd' \mapsto SOME(x, \#hd) * is\_list(hd, xs) \rangle$$

pop

$$\langle xs, hd. s \mapsto \#hd* is\_list(hd, xs) \rangle \\
  pop(\#s, x) \\
  \langle ret. (ret = NONE \land xs = [] * s \mapsto \#hd * is\_list(hd, [])) \lor \\
               (\exists x, xs', hd'.ret = SOME(x) \land xs = x::xs' * s \mapsto \#hd' * hd \mapsto_q SOME(x, \#hd') * is\_list(hd', xs'))\rangle$$

### invariant ones


## Protocol

The protocol is based on the previous prototype of a simple helping example. The major difference is:

1. Some of the ghost names are per-item, thus existentially packed inside the per-item invariant of the stack;
2. One ghost name is global and locked, which will be used my the *sole* server.
3. The precondition and post-condition are global, arbitrary timeless conditions that qualify over request. A frame `R` is also added to implement the syncer style spec.

![](st.png)

## Problems

The major problem is current flat combiner spec qualifies over a fixed `P` and `Q` in the syncer style spec I derived, which is much more restricted than the universally qualified version. 

The reason why this happens is simple: The `P Q` are encoded as part of the per-item invariant, that is to say, we enforce that for each item the `P, Q` in its state transitions are all the same.

I tried to encode any `P Q` and a hoare triple involving `P, Q, f` inside the *INSTALLED* state. But it seems difficult to confirm that the final `y` satisfies the same `Q`: because when we installed `Q`, we know what `Q` is, but when it is installed, it is existentially qualified, and same till the time of $FINISHED$ state. Thus, when we open the $\exists Q, Q(x, y)$, we don't know if $Q' = Q$.


## Stat

`flat.v`: 440 lines, 1 minute and 30 seconds.

`treiber_stack.v`: 450 lines

`misc.v`: 200 lines