# Claims about Cached Opsem

## Background

Let us first define the following types

PermScore: [0,1]
Register: String
Address: Natural
Location -> Register | Address
M : Location -> Address, (Parent, PermScore)

Each Pointer (in a register or memory) has a `PermScore` between [0, 1].

- A score of 1 means sole access to the memory location it points to -- hence read-write access.
- A score of 0 implies that the pointer is dormant - it points to a memory location but cannot read or write.
- A score between 0 and 1 means that the pointer can read but not write memory.

Our first claim is:

**Claim 1** An allocated memory region has a total `PermScore` of 1.0 distributed between all pointers to the memory region.

Proof:

Assume `alloc` creates a pointer with `PermScore` 1.0 and `ps: Location -> [0,1]`.

{ps(p) == 0}  ---- (0)
alloc(p, sz)
{ps(p) == 1}

Now if we can prove that all operations on pointers distribute `PermScore` between pointers to the same location then we can prove Claim 1. The different operations are:
1. `alloc`;
2. `brreg2reg`;
3. `brmem2reg`;
4. `brmem2reg_ro`;
5. `mvmem2reg`;
6. `mvreg2mem`;
7. `die`.

We write our goal as:

**Claim 1.1** All operations on pointers maintain Claim 1.

Proof:

Let us define the following invariants.

{ps(taker) == 0, ps(giver) = X, 0 <= X <= 1}  ---- (1)
takePerm(giver, taker)
{ps(giver) == 0, taker == X}

{ps(giver) == X, ps(taker) = Y, 0 <= X + Y <= 1}  ---- (2)
returnPerm(giver, taker)
{ps(giver) = 0, ps(taker) = X + Y}

{ps(giver) == X, ps(taker) = 0, 0 <= X <= 1}  ---- (3)
splitPerm(giver, taker)
{ps(giver) = X/2, ps(taker) = X/2}

Let us now look at how each operation holds Claim 1. Once we show that all of them hold, then inductively the claim will hold in any valid program.

#### p1, q0 = brreg2reg p0

To prove:
{ps(p1) == 0, ps(q0) == 0, ps(p0) == 1 }
brreg2reg(p0, q0, p1) 
{ps(p1) == 0, ps(q0) == 1, ps(p0) == 0 }

Operationally `brreg2reg` does the following
1. takePerm(p0, q0)

Solving for ?:
Thus {ps(p1) == 0, ps(q0) == 0, ps(p0) == 1 } takePerm(p0, q0) {?}
Using (1) we can rewrite as
{ps(p1) == 0, ps(q0) == 0, ps(p0) == 1 } takePerm(p0, q0) {ps(p1) == 0, ps(q0) == 1, ps(p0) == 0}

#### m1, q0 = brmem2reg pp0, m0

To prove:
{ps(m0[pp0]) == 1, ps(q0) == 0 }
brmem2reg(q0, pp0, m0) -> m1
{ps(m0[pp0]) == 0, ps(q0) == 1, ps(m1[pp0]) == 0 }

Operationally `brmem2reg` does the following
1. takePerm(m0[pp0], q0)

Solving for ?:
Thus {ps(m0[pp0]) == 1, ps(q0) == 0 } takePerm(m0[pp0], q0) {?}
Using (1) we can rewrite as
{ps(m0[pp0]) == 1, ps(q0) == 0 } takePerm(m0[pp0], q0) {ps(m0[pp0]) == 0, ps(q0) == 1, ps(m1[pp0]) == 0 }

#### m1, q0 = brmem2reg_ro pp0, m0

To prove:
{ps(m0[pp0]) == X, ps(q0) == 0, 0 <= X <= 1 }
brmem2reg_ro(q0, pp0, m0) -> m1
{ps(m0[pp0]) == 0, ps(q0) == X/2, ps(m1[pp0]) == X/2 }

Operationally `brmem2reg_ro` does the following
1. splitperm(m0[pp0], q0)

Solving for ?:
Thus {ps(m0[pp0]) == X, ps(q0) == 0, 0 <= X <= 1} splitPerm(m0[pp0], q0) {?}
Using (3) we can rewrite as
{ps(m0[pp0]) == X, ps(q0) == 0, 0 <= X <= 1} splitPerm(m0[pp0], q0) {ps(m0[pp0]) == 0, ps(q0) == X/2, ps(m1[pp0]) == X/2 }

#### m1 = mvreg2mem pp0, p0, m0

To prove:
{ps(m0[pp0]) == 0, ps(p0) == 1 }
mvreg2mem(p1, pp0, m0) -> m1
{ps(m0[pp0]) == 0, ps(p1) == 0, ps(m1[pp0]) == 1 }

Operationally `mvreg2mem` does the following
1. takePerm(p0, m[pp0])

Solving for ?:
Thus {ps(m0[pp0]) == 0, ps(p0) == 1} takePerm(p0, m[pp0]) {?}
Using (1) we can rewrite as
{ps(m0[pp0]) == 0, ps(p0) == 1} takePerm(m0[pp0], q0) {ps(m0[pp0]) == 0, ps(q0) ==0, ps(m1[pp0]) == 1 }

#### m1, p1 = mvmem2reg pp0, m0

To prove:
{ps(m0[pp0]) == 1, ps(p1) == 0 }
mvmem2reg(p1, pp0, m0) -> m1
{ps(m0[pp0]) == 0, ps(p1) == 1, ps(m1[pp0]) == 0 }

Operationally `mvmem2reg` does the following
1. takePerm(m[pp0], p1)

Solving for ?:
Thus {ps(m0[pp0]) == 1, ps(p1) == 0} takePerm(p0, m[pp0]) {?}
Using (1) we can rewrite as
{ps(m0[pp0]) == 1, ps(p1) == 0} takePerm(m0[pp0], q0) {ps(m0[pp0]) == 0, ps(p1) == 1, ps(m1[pp0]) == 0 }

#### die q0

`pr(p) gives the parent of pointer p or None`

To prove:
{ps(q0) = X, ps(pr(q0)) = Y, 0 <= X + Y <= 1 }
die (q0, m0) -> m1
{ps(q0) = 0, ps(pr(q0)) = X + Y }

Operationally `die` does the following
1. returnPerm(q0, ps(pr(q0)))

Solving for ?:
Thus {ps(q0) = X, ps(pr(q0)) = Y, 0 <= X + Y <= 1 } returnPerm(q0, ps(pr(q0))) {?}
Using (1) we can rewrite as
{ps(q0) = X, ps(pr(q0)) = Y, 0 <= X + Y <= 1 } returnPerm(q0, ps(pr(q0))) {ps(q0) = 0, ps(pr(q0)) = X + Y }

Here Claim 1.1 is proved and therefore Claim 1 is proved.

### More claims

**Claim 2** If a pointer to an allocated region has `PermScore` 1.0 then all other pointers (if any) have `PermScore` 0.

Proof:
By counter example: Let us say we have two pointers A and B where A has a `PermScore` 1.0 and B has `PermScore` > 0.0 then `ps(A) + ps(B) > 1` which violates Claim 1.

**Claim 3** If a pointer to an allocated region has 0.0 < `PermScore` < 1.0 then all other pointers must have 0 <= `PermScore` < 1.0 such that the cumulative `PermScore` is 1.0.

Proof:
By counter example
Let us say there are `n` pointers `p0, ..., pn-1` to a memory location. Let 0.0 < ps(p0) < 1.0 without loss of generality. Now assume there is another pointer pm (0 <= m <=n) such that ps(pm) = 1. Now `ps(p0) + ... + ps(pm) + ... + pn-1 > 1` which violates Claim 1.

**Claim 4** If a pointer to an allocated region has `PermScore` 0.0 then there must be at least one other pointer to the allocated region with `PermScore` > 0.0.

Proof:
We can prove by counterexample.

## Mapping distributed state to centralized state

> Note: This section has different nomenclature than above. It may be read independently modulo proofs for mentioned claims.

The procedure to map distributed state to centralized state follows:

1. The D machine has a single store M_D which maps `Location -> Address * Cache Value * (Parent, PermScore)`. Each Location is (Register | Address) i.e. a union of register file and main memory.
2. To map M_D to <R, M, S, O>, we go through all Locations in M_D. For each key l,
* we copy the corresponding address to either R or M in C.
* we copy the correct cache value to S. If multiple keys map to the same key in S then either the cache value must be the same (since no pointer has RW access as per Claim 3) or only one-of-N pointers is active and its value dominates (Claim 2) .
* similar to cache value, for each l we set the appropriate ownership state in O. That is, either the state is immutably borrowed or uniquely owned.
3. At the end of this construction, the distributed state of D is mapped to the centralized state of C.

## How does the distributed machine know what is the latest value in the centralized machine?

1. Given a pointer P, if ps(P) or ps(M_D[P]) is (0,1] then return cached value else goto step 2.
2. Go through all pointers in memory until another pointer to the same address is found. Goto step 1.

**Claim 5**
Since `PermScore` of all pointers to a memory location cannot be 0.0 as per Claim 4, the recursion will eventually terminate.