Massachusetts Institute of Technology Lecture 10 6.042J/18.062J: Mathematics for Computer Science October 12, 2000 Professors Nancy Lynch and Shlomi Dolev

Composing and Decomposing Computational Processes

1 Externally-visible behavior

1.1 Dynamic Set

Q: fun, a function from S to {0, 1}.

req, either add(v), delete(v), lookup(v), or null, which represents no active request resp, either OK , a Boolean b, or null, which indicates no ready response.

Q_{0}: fun: As before, the function that maps everything to 0, representing the empty set. req: null resp: null

δ: Input steps:

request(add(v)): Can occur anytime Effect: if req = null then req := add(v) And similarly for the other two kinds of inputs.

Internal steps: perform(add(v)): Can occur if: req = add(v) and resp = null Effect is to set fun(v) to 1 and resp to OK

perform(delete(v)) Can occur if: req = delete(v) and resp = null Effect: fun(v) := 0; resp := OK

perform(lookup(v)): Can occur if: req = lookup(v) and resp = null Effect: resp := fun(v)

Output steps: respond(r): Can occur if: resp = r Effect: req := null, resp := null

1.2 Caching

Weak caching:

Q: mem, cache, same types as before req, a mapping from I (locations) to the set of values {read(a), write(a, v), null} resp, a mapping from I to the set of values V (the value set) ∪{OK null}

Q_{0}: mem everywhere v_{0}, cache everywhere null, bookkeeping components all null L: Input:

request(read(a), i), a ∈ A, i ∈ I
request(write(a, v), i), a ∈ A, v ∈ V, i ∈ I

Internal:

perform(read(a), i), a ∈ A, i ∈ I

perform(write(a, v), i), a ∈ A, v ∈ V, i ∈ I
copy(a, i), a ∈ A, i ∈ I
drop(a, i), a ∈ A, i ∈ I

Output:

respond(v, i), v ∈ V, i ∈ I

respond(OK , i), i ∈ I

δ: request(read(a), i)

Can occur: anytime Effect: if req(i) = null then req(i) := read(a)

request(write(a, v), i) Can occur: anytime Effect: if req(i) = null then req(i) := write(a, v)

perform(read(a), i), a ∈ A, i ∈ I Can occur: req(i) = read(a), cache(a, i) ≠ null, and resp(i) = null Effect: resp(i) := cache(a, i)

perform(write(a, v), i) Can occur: req(i) = write(a, v) and resp(i) = null Effect: mem(a) := v; resp(i) := OK

copy(a, i) Can occur: anytime Effect: cache(a, i) := mem(a)

drop(a, i) Can occur: anytime Effect: cache(a, i) := null

respond(r, i) Can occur: resp(i) = r Effect: req(i) := null; resp(i) := null

Strong caching, same except for:

perform(write(a, v), i) Can occur: req(i) = write(a, v) and resp(i) = null Effect: mem(a) := v; for all i, cache(a, i) := null; resp(i) := OK

2 Implementation

2.1 Dynamic set

Q: dynamic-set, a subset of S

req, resp, as before Q_{0}: dynamic-set: ∅

req, resp: null L: As before. δ: Inputs, outputs: As before.

Internal steps: perform(add(v)): Can occur if: req = add(v) and resp = null Effect: dynamic-set := dynamic-set ∪ {v}; resp := OK

perform(delete(v)) Can occur if: req = delete(v) and resp = null Effect: dynamic-set := dynamic-set − {v}; resp := OK

perform(lookup(v)): Can occur if: req = lookup(v) and resp = null Effect: if v ∈ dynamic-set then resp := 1 else resp := 0

2.2 Caching example

Centralized memory machine:

Q: mem, req, resp, same types as for SC Q_{0}: As for SC . L: Input, Output: As for SC .

Internal:

perform(read(a), i), a ∈ A, i ∈ I

perform(write(a, v), i), a ∈ A, v ∈ V, i ∈ I

Transitions:

Input, Output: As for SC . Internal: perform(read(a), i) Can occur: req(i) = read(a) and resp(i) = null Effect: resp(i) := mem(a)

perform(write(a, v), i) Can occur: req(i) = write(a, v) and resp(i) = null Effect: mem(a) := v; resp(i) := OK

3 Abstraction relations and the Abstraction Theorem

Definition 3.1 Suppose A and B are labeled state machines with the same input and output labels. Then a relation R from states of A to states of B is called an abstraction relation from A to B provided that the following conditions hold:

1. (Start condition) If q_{A} is a start state of A, then there exists a start state q_{B} of B such that (q_{A}, q_{B}) ∈ R.

2. (Step condition) If q_{A} and q_{B} are reachable states of A and B, respectively, (q_{A}, q_{B}) ∈ R, and (q_{A}, ℓ, q′_{A}) is a step of A, then there is a sequence of (0 or more) steps of B that:

– Starts with q_{B},

– Ends with some state q′_{B} such that (q′_{A}, q′_{B}) ∈ R, and

– Has the same trace as the step of A (that is, it looks the same externally).

4 Composition

Environment automaton, for Split-SC

Q: locks, a mapping from A to subsets of I Q_{0}: for all a, locks(a) = ∅ L: Reverse of Split-SC :

Input:

respond(v, i), v ∈ V, i ∈ I
respond(OK , i), i ∈ I

Output:

request(read(a), i), a ∈ A, i ∈ I

request(write(a, v), i), a ∈ A, v ∈ V, i ∈ I

Transitions:

respond(∗, i) Can occur: anytime Effect: for all a, locks(a) := locks(a) − {i}

request(read(a), i) Can occur: locks(a) = ∅ Effect: locks(a) := {i}

request(write(a, v), i) Can occur: locks(a) = ∅ Effect: locks(a) := {i}