## A.2 Parallel Execution and Shared Variable Resynchronization

Before proving that all ForeC kernel programs are deterministic, we prove that threads execute their local ticks in isolation, and that the aggregation of states and the semantic function COMBINE are both deterministic. These are captured by Lemmas 8, 10, and 11 below, with the assumption that all the combine functions are deterministic. We further prove in Lemmas 13 and 15 that the associative and commutative property of the par statement is dependent on combine functions having the same respective properties.

**DEFINITION 5.** A **combine function** $cf: D \times D \rightarrow D$ is any C function with two input values $v_1$ and $v_2$ of identical type, which returns a value of the same type.

**DEFINITION 6.** A **combine function** $cf$ is **deterministic** if there exists only one value that can be returned for a given set of input values:

$$ \forall v_1, v_2 \in D \times D, \exists! v_3 \in D \text{ such that } cf(v_1, v_2) = v_3 $$

From now on, we assume that every combine function $cf$ always terminates and is deterministic, regardless of the program's current state.

**ASSUMPTION 7.**

$$ \forall S, S', I, t, v_1, v_2, cf: \quad EVAL(S.E, I, t, cf(v_1, v_2)) = EVAL(S'.E, I, t, cf(v_1, v_2)) $$

**LEMMA 8.** Every thread executes their local ticks in **isolation**, i.e., when a thread executes its local tick, it cannot modify the variables of any other thread and it cannot observe the modifications of any other thread.

**PROOF.** Recall from Section 3.2 that $E[G]$ stores all the output, shared, and private variables of the program, while $E[t]$ stores the copies of the shared variables of thread $t$. The requirement for a private variable not to appear in the body of more than one thread can be ensured via static type checking. Recall that threads always create copies of shared variables at the start of their local tick via the copy kernel construct and the COPY semantic function (Section 3.3.3).

Let $t$ be a thread that writes value $v$ to variable $var$ during its local tick. This is only possible via the (assign-private) and (assign-shared) rules:

**Private variable:** In the (assign-private) rule, $v$ is assigned directly to the private variable, i.e., $E[G][var]$. Static type checking ensures that no other thread can also write to variable $var$.

**Shared variable:** In the (assign-shared) rule, $v$ is only assigned to the thread's copy of the shared variable, i.e., $E[t][var]$. It is not possible to write to another thread's copy.

Let $t'$ be a thread that reads value $v'$ from variable $var'$ during its local tick. This is only possible via the (status), (assign-shared), (assign-private), (if-then), (if-else), (loop-then), and (loop-else) rules, which rely on the GETVAL semantic function (Section 3.3.2). The value that GETVAL returns depends on whether $var'$ is a shared or private variable (see Algorithm 1):

**Shared variable:** In Algorithm 1, the value is returned from the thread's copy of the shared variable, i.e., $E[t'][var']$. It is not possible to read from another thread's copy.

**Private variable:** In Algorithm 1, the value is returned directly from the private variable, i.e., $E[G][var']$, because the COPY semantic function (Section 3.3.3) never makes copies of private variables.

In conclusion, each thread executes its local tick in isolation because (1) no thread can access the private variables belonging to other threads, and (2) a thread can only access (read and write) its own copies of the shared variables. □
**DEFINITION 9.** The aggregation of states $S'$ and $S''$ into a single state $S^A$ is **deterministic** if there exists only one possible $S^A$. Let $\odot$ be the binary operator denoting the aggregation of states, then

$$ \forall S', S'', \exists! S^A \text{ such that } S^A = S' \odot S'' $$

**LEMMA 10.** Let $t_1: f_1$ and $t_2: f_2$ be two ForeC kernel threads that are correct with respect to syntax and type checking. Let the initial state be $S = \langle E, A \rangle$ and the resulting states be $S' = \langle E', A' \rangle$ and $S'' = \langle E'', A'' \rangle$ such that

$$ \langle S \rangle t_1 : f_1 \xrightarrow{k'} \langle S' \rangle t_1 : f_1' \quad \text{and} \quad \langle S \rangle t_2 : f_2 \xrightarrow{k''} \langle S'' \rangle t_2 : f_2'' $$

The aggregation of states $S^A = S' \odot S''$ is deterministic.

Recall from Section 3.4.10 that the aggregation $S^A = \langle E^A, A^A \rangle$ is defined as:

$$ E^A = (E' \setminus (E' \cap E)) \cup (E'' \setminus (E'' \cap E)) \cup (E' \cap E'') \quad \text{and} $$

$$ A^A = (A' \setminus (A' \cap A)) \cup (A'' \setminus (A'' \cap A)) \cup (A' \cap A'') $$

**PROOF.** We begin by proving that the aggregation of environments $E'$ and $E''$ is deterministic. The intersection $(E' \cap E'')$ contains all variables that have not changed from $E$. The two complements are the subsets $E_1 = (E' \setminus (E' \cap E))$ and $E_2 = (E'' \setminus (E'' \cap E))$ that contain all the variables that have changed from $E$. To prove that the aggregation is deterministic, it is sufficient to prove that $E_1 \cap E_2 = \emptyset$:

**Private variables** of threads $t_1$ and $t_2$ that have changed are in $E_1[G]$ and $E_2[G]$, respectively. Thanks to Lemma 8 we know that $t_1$ and $t_2$ cannot access the same private variables, thus, $E_1[G] \cap E_2[G] = \emptyset$.

**Copies of shared variables** for threads $t_1$ and $t_2$ belong in $E_1[t_1]$ and $E_2[t_2]$, respectively. Thanks to Lemma 8 we know that $t_1$ and $t_2$ can only access their own copies of shared variables and never the copies of other threads, thus, $\forall t \in T : E_1[t] \cap E_2[t] = \emptyset$.

We now prove that the aggregation of preemption statuses $A'$ and $A''$ is deterministic. The intersection $(A' \cap A)$ contains all preemption statuses that have not changed from $A$. The two complements are the subsets $A_1 = (A' \setminus (A' \cap A))$ and $A_2 = (A'' \setminus (A'' \cap A))$ that contain all the preemption statuses that have changed from $A$. To prove that the aggregation is deterministic, it is sufficient to prove that $A_1 \cap A_2 = \emptyset$: A thread can only change the preemption status of an abort identifier by executing a status statement (see the (status) rule). By construction, a unique abort identifier is passed into every status statement, thus, $A_1 \cap A_2 = \emptyset$.

In conclusion the aggregation of $S'$ and $S''$ into $S^A$ is deterministic because only the unions of disjoint sets are taken. $\square$

**LEMMA 11.** The semantic function COMBINE($E$, $t_1$, $t_2$, $t_0$) is deterministic: there exists only one environment that it can return for a given set of inputs.

**PROOF.** Algorithm 3 of the semantic function COMBINE initializes all its local variables ($preVal$, $T$, $cf$, $v$), is side-effect-free, and uses only deterministic instructions. In particular, line 11 in Algorithm 3 is deterministic thanks to Assumption 7 (all combine functions $cf$ are deterministic), and because values are passed into $cf$ in a fixed order. Hence, the semantic function COMBINE is deterministic. $\square$
**DEFINITION 12.** The par statement is associative if, in any state S, for any thread bodies $f_a$, $f_b$, and $f_c$, the following holds:

$$ \langle S \rangle t_0 : \mathrm{par}(t_1 : f_a, t_2 : \mathrm{par}(t_3 : f_b, t_4 : f_c)) \xrightarrow{I} \langle S' \rangle t_0 : \mathrm{par}(t_1 : f'_a, t_2 : \mathrm{par}(t_3 : f'_b, t_4 : f'_c)), $$

$$ \langle S \rangle t_0 : \mathrm{par}(t_1 : \mathrm{par}(t_2 : f_a, t_3 : f_b), t_4 : f_c) \xrightarrow{I} \langle S' \rangle t_0 : \mathrm{par}(t_1 : \mathrm{par}(t_2 : f'_a, t_3 : f'_b), t_4 : f'_c). $$

**LEMMA 13.** The par($t_1:f_1$, $t_2:f_2$) statement is associative if and only if the combine functions of involved in combining shared variables are also associative.

**PROOF.** The (par-1) and (par-4)-(par-7) rules require the states of threads $t_1$ and $t_2$ to be aggregated before the shared variables are combined. From Lemma 10, we know that the aggregation is simply the union of disjunct changes to the states, which does not affect the associativity of the par.

By inspecting the (par-1) and (par-4)-(par-7) rules, the semantic function COMBINE is only applied to threads $t_1$ and $t_2$'s copies of shared variables in the aggregated environment $E^A$. In Algorithm 3, the combine policy is applied to each copy individually (lines 4–8), and the combine function of is invoked (line 11) if the combine policy allows both copies to be combined. Because the copies are passed to of in the same textual order that their threads appear in the par statement, the par statement is associative if and only if of is associative. □

**DEFINITION 14.** The par statement is commutative if, in any state S, for any thread bodies $f_a$ and $f_b$, the following holds:

$$ \langle S \rangle t_0 : \mathrm{par}(t_1 : f_a, t_2 : f_b) \xrightarrow{I} \langle S' \rangle t_0 : \mathrm{par}(t_1 : f'_a, t_2 : f'_b), $$

$$ \langle S \rangle t_0 : \mathrm{par}(t_2 : f_b, t_1 : f_a) \xrightarrow{I} \langle S' \rangle t_0 : \mathrm{par}(t_2 : f'_b, t_1 : f'_a). $$

**LEMMA 15.** The par($t_1:f_1$, $t_2:f_2$) statement is commutative if and only if the combine functions of involved in combining shared variables are also commutative.

**PROOF.** Similar to the proof of associativity (Lemma 13), we know that the aggregation of thread states is simply the union of disjunct changes, which does not affect the commutativity of the par. In Algorithm 3 for the semantic function COMBINE, the combine function of is invoked (line 11) with both copies passed in the same textual order as their threads in the par statement. Hence, the par statement is commutative if and only if of is commutative. □

## A.3 Determinism of ForeC Kernel Programs

Equipped with the proof that shared variables are always combined deterministically (Lemma 11), we are ready to prove that ForeC kernel programs are deterministic.

**DEFINITION 16.** A program $t : f$ is **deterministic** if, in any state S, for any input configuration I, there exists at most one transition such that:

$$ \forall S, I: \quad \begin{array}{l} \text{if } \langle S \rangle t : f \xrightarrow{I} \langle S' \rangle t : f' \text{ and } \langle S \rangle t : f \xrightarrow{I} \langle S'' \rangle t : f'' \\ \text{then } S' = S'', f' = f'', k' = k'' \end{array} $$

**THEOREM 17.** Let Assumption 7 be satisfied and let $t : f$ be a ForeC kernel program that is correct with respect to syntax and type checking. Then, any such $t : f$ is **deterministic**.

**PROOF.** The proof can be shown by structural induction on $t : f$.
**Base cases:** The (nop), (copy), (pause), and (status) rules imply that the following kernel statements have at most one transition:

$$ \langle S \rangle t : \text{nop} \xrightarrow{0} \langle S \rangle t : $$

$$ \langle S \rangle t : \text{copy} \xrightarrow{0} \langle S' \rangle t : \text{nop} $$

$$ \langle S \rangle t : \text{pause} \xrightarrow{1} \langle S \rangle t : \text{copy} $$

$$ \langle S \rangle t : \text{status}(a, \exp) \xrightarrow{0} \langle S' \rangle t : \text{nop} $$

The assignment, `if-else`, and `while` kernel constructs are each described by a pair of rewrite rules with complementary premises that do not depend on other transitions: respectively (assign-shared) and (assign-private), (if-then) and (if-else), and (loop-then) and (loop-else). This implies that these kernel constructs have at most one transition:

$$ \text{if } var \in \text{GETSHARED}(t) \text{ then } \langle S \rangle t : var = \exp \xrightarrow{0} \langle S' \rangle t : $$

$$ \text{otherwise } \langle S \rangle t : var = \exp \xrightarrow{0} \langle S'' \rangle t : $$

$$ \text{if } \text{EVAL}(S.E, I, t, \exp) \neq 0 \text{ then } \langle S \rangle t : \text{if } (\text{exp}) f_1 \text{ else } f_2 \xrightarrow{1} \langle S \rangle t : f_1 $$

$$ \text{otherwise } \langle S \rangle t : \text{if } (\text{exp}) f_1 \text{ else } f_2 \xrightarrow{1} \langle S \rangle t : f_2 $$

$$ \text{if } \text{EVAL}(S.E, I, t, \exp) \neq 0 \text{ then } \langle S \rangle t : \text{while } (\text{exp}) f \xrightarrow{1} \langle S \rangle t : f; \text{ while } (\text{exp}) f $$

$$ \text{otherwise } \langle S \rangle t : \text{while } (\text{exp}) f \xrightarrow{0} \langle S \rangle t : $$

Among the rewrite rules considered in the base case, only the (copy), (status), (assign-shared), and (assign-private) rules make direct changes to the state S. The (copy) rule changes only the store E[t] of the executing thread t. This can be verified by inspecting Algorithm 2 of the semantic function COPY. By construction, each status statement has a unique abort identifier a. Thus, the (status) rule never changes the status of an abort identifier more than once. The (assign-shared) rule changes only the store E[t] of the executing thread t. The (assign-private) rule changes only the private variables in E[G] of the executing thread.

**Induction step:** The sequence operator (;), `abort`, and `par` kernel statements allow the composition of kernel constructs. For some $t_1 : f_1$ and $t_2 : f_2$ that are arbitrary compositions of kernel constructs, assume the induction hypotheses that they each have at most one transition:

$$ \text{If } \exists S'_1, S''_1, f'_1, f''_1, k'_1, k''_1 \text{ such that } \langle S_1 \rangle t_1 : f_1 \xrightarrow{k'_1} \langle S'_1 \rangle t_1 : f'_1 \quad (\text{H3}) $$

$$ \text{and } \langle S_1 \rangle t_1 : f_1 \xrightarrow{k'_1} \langle S''_1 \rangle t_1 : f''_1 $$

$$ \text{then } S'_1 = S''_1, f'_1 = f''_1, k'_1 = k''_1 $$

$$ \text{If } \exists S'_2, S''_2, f'_2, f''_2, k'_2, k''_2 \text{ such that } \langle S_2 \rangle t_2 : f_2 \xrightarrow{k'_2} \langle S'_2 \rangle t_2 : f'_2 \quad (\text{H4}) $$

$$ \text{and } \langle S_2 \rangle t_2 : f_2 \xrightarrow{k''_2} \langle S''_2 \rangle t_2 : f''_2 $$

$$ \text{then } S'_2 = S''_2, f'_2 = f''_2, k'_2 = k''_2 $$
Next, we show that the sequence operator (;), and the abort and par kernel statements have at most one transition.

(1) Consider the fragment $t_1 : f_1; f_2$. By induction hypothesis (H3), there is only one possible transition for the fragment $t_1 : f_1$, which is either:

$$ \langle S_1 \rangle t_1 : f_1 \xrightarrow{k_1=0} \langle S'_1 \rangle t_1 : $$

or:

$$ \langle S_1 \rangle t_1 : f_1 \xrightarrow{k_1 \in \{1, \perp\}} \langle S'_1 \rangle t_1 : f'_1 $$

The table below shows that at most one sequence rule can be applied depending on the completion code $k_1$:

<table><tr><td colspan="3"><i>k</i><sub>1</sub></td></tr><tr><td><b>0</b></td><td><b>1</b></td><td><b>&perp;</b></td></tr><tr><td>(seq-right)</td><td>(seq-left)</td><td></td></tr></table>

It follows that the sequence operator “;” is deterministic.

(2) Consider the abort kernel statement in the fragment $t_1 : \text{weak? abort}(a_1, f_1)$. By induction hypothesis (H3), there is only one possible transition for the program fragment $t_1 : f_1$, which is either:

$$ \langle S_1 \rangle t_1 : f_1 \xrightarrow{k_1=0} \langle S'_1 \rangle t_1 : $$

or:

$$ \langle S_1 \rangle t_1 : f_1 \xrightarrow{k_1 \in \{1, \perp\}} \langle S'_1 \rangle t_1 : f'_1 $$

The table below shows that at most one abort rule can be applied depending on the completion code $k_1$ and the preemption status $A[a_1]$:

<table><thead><tr><th rowspan="2"></th><th colspan="3">Strong abort, k<sub>1</sub></th><th colspan="3">Weak abort, k<sub>1</sub></th></tr><tr><th>0</th><th>1</th><th>&perp;</th><th>0</th><th>1</th><th>&perp;</th></tr></thead><tbody><tr><th rowspan="2">A[a<sub>1</sub>]</th><td>= 0</td><td>(abort-2)</td><td>(abort-1)</td><td>(abort-2)</td><td colspan="2">(abort-1)</td></tr><tr><td>&ne; 0</td><td colspan="2">(abort-6)</td><td>(abort-3)</td><td>(abort-5)</td><td>(abort-4)</td></tr></tbody></table>

It follows that the abort kernel statement is deterministic.

(3) Consider the par kernel statement in the fragment $t : \text{par}(t_1 : f_1, t_2 : f_2)$. By induction hypotheses (H3) and (H4), there is only one possible transition for the program fragment $t_1 : f_1$, which is either:

$$ \langle S_1 \rangle t_1 : f_1 \xrightarrow{k_1=0} \langle S'_1 \rangle t_1 : $$

or:

$$ \langle S_1 \rangle t_1 : f_1 \xrightarrow{k_1 \in \{1, \perp\}} \langle S'_1 \rangle t_1 : f'_1 $$

and there is only one possible transition for the program fragment $t_2 : f_2$, which is either:

$$ \langle S_2 \rangle t_2 : f_2 \xrightarrow{k_2=0} \langle S'_2 \rangle t_2 : $$
or:

$$ \langle S_2 \rangle t_2 : f_2 \xrightarrow{k_2 \in \{1, \perp\} \atop I} \langle S'_2 \rangle t_2 : f'_2 $$

The table below shows that at most one par rule can applied depending on the completion codes $k_1$ and $k_2$:

<table><thead><tr><th></th><th colspan="3">k<sub>2</sub></th></tr><tr><th></th><th>0</th><th>1</th><th>⊥</th></tr></thead><tbody><tr><th rowspan="3">k<sub>1</sub></th><th>0</th><td>(par-5)</td><td>(par-6)</td><td></td></tr><tr><th>1</th><td>(par-7)</td><td>(par-4)</td><td>(par-2)</td></tr><tr><th>⊥</th><td>(par-3)</td><td></td><td>(par-1)</td></tr></tbody></table>

It follows that the par kernel statement is deterministic.

In conclusion, all ForeC kernel programs that are correct with respect to syntax and type checking are deterministic. □
<figure><img src="image_25.png" /><figcaption>(a) ForeC program.</figcaption></figure>

<figure><img src="image_26.png" /><figcaption>(b) Translated kernel program.</figcaption></figure>

<figure><img src="image_27.png" /><figcaption>(c) Control-flow graph.</figcaption></figure>

<caption>Fig. 25. Illustrative example one.</caption>

# B ILLUSTRATIONS

This section illustrates how ForeC programs execute under the formal semantics presented in Section 3.4. Two example ForeC programs are used, and their executions are given as a sequence of rewrites.

## B.1 Example One

The first program illustrates parallel execution using the par statement. Figure 25a presents the ForeC program, and Figure 25c illustrates the program's control-flow. Recall that an upright triangle represents the forking of threads while an inverted triangle represents the joining of threads. The corresponding kernel program is shown in Figure 25b.

In the program's first tick, the parent thread main begins its local tick by forking two child threads, t1 and t2. The child threads start their local ticks by copying the shared variable s. Thread t1 pauses while thread t2 assigns 4 to its local copy of s and terminates. The first tick ends and the shared variable s is resynchronized. Using the combine policy all, the new value (or the resynchronized value) of s becomes plus(0, 4) = 4. In the second tick, only thread t1 is active and it starts its local tick by creating a copy of s, assigning 3 to its copy of s, and then terminating. Now that both child threads have terminated and joined, the par combines its children's copies of s before also terminating. Because only thread t1 was active in the second tick, its copy of s is assigned directly to its parent thread main. Thread main starts its local tick which results in the program terminating. The second tick ends and the shared variable s is resynchronized with the value 3 because only thread main has a copy of s.

Before we apply the rewrite rules to the program, it is structurally translated into the kernel program of Figure 25b (see the start of Section 3). The semantic functions GETSHARED(main), GETSHARED(t1), GETSHARED(t2) and GETSHARED($G$) all return {$s$}. The set of preemption states A is initially $\emptyset$. The program's environment E and its derivatives are defined in Figure 26.

**Step 1:** Start the tick by applying the (seq-right) and (copy) rules.

$$ (\text{seq-right}) \frac{ (\text{copy}) \quad \frac{ (E, A) \text{ main:copy} \xrightarrow{0} (E^1, A) \text{ main:} \quad (\text{copy}) }{ (E, A) \text{ main:copy; par(t1:\{copy; pause;s=3;} , t2:\{copy;s=4;} ) } \xrightarrow{\perp} (E^1, A) \text{ main:par(t1:\{copy; pause;s=3;} , t2:\{copy;s=4;} ) } $$
$$E = \{G \to \{s \to (0, pre)\}\}$$

$$E^1 = \{G \to \{s \to (0, pre)\}, main \to \{s \to (0, pre)\}\}$$

$$E^2 = \{G \to \{s \to (0, pre)\}, main \to \{s \to (0, pre)\}, t1 \to \{s \to (0, pre)\}\}$$

$$E^3 = \{G \to \{s \to (0, pre)\}, main \to \{s \to (0, pre)\}, t2 \to \{s \to (0, pre)\}\}$$

$$E^4 = \{G \to \{s \to (0, pre)\}, main \to \{s \to (0, pre)\}, t1 \to \{s \to (0, pre)\}, t2 \to \{s \to (0, pre)\}\}$$

$$E^5 = \{G \to \{s \to (0, pre)\}, main \to \{s \to (0, pre)\}, t1 \to \{s \to (0, pre)\}, t2 \to \{s \to (4, mod)\}\}$$

$$E^6 = \{G \to \{s \to (0, pre)\}, main \to \{s \to (4, cmb)\}\}$$

$$E^7 = \{G \to \{s \to (4, pre)\}\}$$

$$E^8 = \{G \to \{s \to (4, pre)\}, t1 \to \{s \to (4, pre)\}\}$$

$$E^9 = \{G \to \{s \to (4, pre)\}, t1 \to \{s \to (3, mod)\}\}$$

$$E^{10} = \{G \to \{s \to (4, pre)\}, main \to \{s \to (3, cmb)\}\}$$

$$E^{11} = \{G \to \{s \to (3, pre)\}\}$$

<caption>Fig. 26. Initial program environment and its derivatives.</caption>

**Step 2:** Both threads of the par execute sequential statements, both starting with a copy statement. Apply the (par-1) rule. Additionally, apply the (seq-right) and (copy) rules to both threads. The environments of both threads, $E^2$ and $E^3$, are aggregated into $E^4$.

$$ \begin{array}{ccc} \text{(copy)} & \frac{\langle E^1, A \rangle \text{ t1: copy} \xrightarrow{0} \langle E^2, A \rangle \text{ t1:}}{\langle E^1, A \rangle \text{ t1: copy; } \substack{\xrightarrow{\perp} \\ \text{pause}; s=3}} & \text{(copy)} \frac{\langle E^1, A \rangle \text{ t2: copy} \xrightarrow{0} \langle E^3, A \rangle \text{ t2:}}{\langle E^1, A \rangle \text{ t2: copy}; s=4; \substack{\xrightarrow{\perp} \\ \text{t2:} s=4;}} \\ \text{(seq-right)} & \frac{\langle E^1, A \rangle \text{ t1: copy; } \substack{\xrightarrow{\perp} \\ \text{pause}; s=3}}{\langle E^1, A \rangle \text{ t1: pause; s=3}} & \text{(seq-right)} \frac{\langle E^1, A \rangle \text{ t2: copy; } \substack{\xrightarrow{\perp} \\ \text{pause}; s=3;}}{\langle E^1, A \rangle \text{ t2: copy}; s=4; \substack{\xrightarrow{\perp} \\ \text{t2:} s=4;}} \end{array} $$

**Step 3:** Apply the (tick) and (par-7) rules. Additionally, apply the (seq-left) and (pause) rules to the first thread and the (assign-shared) rule to the second thread. **The program completes the tick.** Note that when the (par-7) rule is applied, the aggregation of environments $E^4$ and $E^5$ is simply $E^5$, whose stores for threads t1 and t2 are combined into thread main's store, resulting in $E^6$. When the (tick) rule is applied, $E^6$ is resynchronized to be $E^7$.

$$ \begin{array}{ccc} \text{(pause)} & \frac{\langle E^4, A \rangle \text{ t1: } \substack{\xrightarrow{1} \\ \text{pause}}}{} & \langle E^4, A \rangle \text{ t1: } \substack{\xrightarrow{1} \\ \text{copy}}}{} \\ \text{(seq-left)} & \frac{\langle E^4, A \rangle \text{ t1: } \substack{\xrightarrow{1} \\ \text{pause}; s=3}}{} & \langle E^4, A \rangle \text{ t1: } \substack{\xrightarrow{1} \\ \text{copy}; s=3}}{} \\ \text{(par-7)} & \frac{\langle E^4, A \rangle \text{ main: par}(\text{t1:}\{\text{pause}; \substack{\xrightarrow{1} \\ s=3;}, \text{t2:}\{s=4;\})}}{\langle E^4, A \rangle \text{ main: par}(\text{t1:}\{\text{pause}; \substack{\xrightarrow{1} \\ s=3;}, \text{t2: nop}\})} & \substack{s \in \{s\} \\ \langle E^4, A \rangle \text{ t2: } \substack{\xrightarrow{0} \\ s=4;}} \frac{\langle E^5, A \rangle \text{ t2: }}{\langle E^5, A \rangle \text{ t2: } \substack{\xrightarrow{0} \\ s=4;}} \\ \text{(tick)} & \frac{\langle E^4, A \rangle \text{ main: par}(\text{t1:}\{\text{pause}; \substack{\xrightarrow{1} \\ s=3;}, \text{t2:}\{s=4;\})}}{\langle E^4, A \rangle \text{ main: par}(\text{t1:}\{\text{pause}; \substack{\xrightarrow{1} \\ s=3;}, \text{t2: nop}\})} & \substack{\langle E^6, A \rangle \text{ main: par}(\text{t1:}\{\text{copy}; \substack{\xrightarrow{1} \\ s=3;}, \text{t2: nop}\}) \\ \langle E^7, A \rangle \text{ main: par}(\text{t1:}\{\text{copy}; \substack{\xrightarrow{1} \\ s=3;}, \text{t2: nop}\})}{} \end{array} $$

**Step 4:** Start the next tick by applying the (par-3) rule. Additionally, apply the (seq-right) and (copy) rules to the first thread and the (nop) rule to the second thread.
<figure><img src="image_28.png" /><figcaption>(a) ForeC program.</figcaption></figure>

<figure><img src="image_29.png" /><figcaption>(b) Translated kernel program.</figcaption></figure>

<figure><img src="image_30.png" /><figcaption>(c) Control-flow graph.</figcaption></figure>

<caption>Fig. 27. Illustrative example two.</caption>

$$ 
\begin{align*}
E &= \{G \to \{x \to (1, pvt)\}\} & A &= \{a1\} \\
E^1 &= \{G \to \{x \to (2, pvt)\}\} & A^1 &= \{a1 \to 1\} \\
     & & A^2 &= \{a1 \to 0\}
\end{align*}
$$

<caption>Fig. 28. Initial program state and its derivatives.</caption>

## B.2 Example Two

The second program illustrates the preemption by using an immediate weak abort statement. Figure 27a presents the ForeC program and Figure 27c illustrates the program's control-flow. Recall that a pair of decorated diamonds represents the scope of an abort body. The corresponding kernel program is shown in Figure 27b.

In the program's first tick, thread main reaches the immediate and weak abort and immediately evaluates the preemption condition (x==1). The condition evaluates to true so the preemption is triggered. Because the abort is weak, the preemption is taken only when the execution of the encapsulated thread reaches the pause, hence, after variable x has been incremented. The abort terminates and, as a result, thread main terminates. At this point, the first tick ends.

Before we apply the rewrite rules to the program, it is structurally translated into the kernel program of Figure 27b (see the start of Section 3). No copy kernel statement is inserted into the program because no shared variables are used. The semantic functions GETSHARED(main) and GETSHARED(G) all return 0. The program's environment E, preemption statuses A, and their derivatives are defined in Figure 28.

**Step 1:** Start the tick by applying the (seq-right) and (status) rules. Note that the abort's preemption is triggered because the condition x==1 evaluates to 1.

$$ (\text{seq-right}) \frac{(\text{status})}{\langle E, A \rangle \text{ main: status(a1, x==1)}} \xrightarrow{0} \langle E, A^1 \rangle \text{ main:} \\ \frac{\langle E, A \rangle \text{ main:status(a1, x==1); weak abort(a1, \{x++;pause;\})}}{I} \xrightarrow{\perp} \langle E, A^1 \rangle \text{ main:weak abort} \\ \qquad (a1, \{x++;pause;\}) $$

**Step 2:** Apply the (abort-4), (seq-right), and (assign-private) rules.
$$
\begin{array}{l}
(\text{assign-private}) \quad \frac{x \notin \emptyset}{\langle E, A^1 \rangle \text{ main:}x++ \xrightarrow{0} \langle E^1, A^1 \rangle \text{ main:}} \\
(\text{seq-right}) \quad \frac{\langle E, A^1 \rangle \text{ main:}x++; \text{pause} \xrightarrow{\perp} \langle E^1, A^1 \rangle \text{ main:pause}}{\langle E, A^1 \rangle \text{ main:}x++; \text{pause} \xrightarrow{\perp} \langle E^1, A^1 \rangle \text{ main:weak abort}} \\
(\text{abort-4}) \quad \frac{\langle E, A^1 \rangle \text{ main:weak abort} \xrightarrow{\perp} \langle E^1, A^1 \rangle \text{ main:weak abort}}{\langle E, A^1 \rangle \text{ main:weak abort}(a1, \{x++;pause;\}) \xrightarrow{\perp} \langle E^1, A^1 \rangle \text{ main:copy}}
\end{array}
\quad (A^1[a1] \neq 0)
$$

Step 3: Apply the (abort-5) and (pause) rules. Note that the preemption is taken because the abort's body has reached a pause.

$$
(\text{pause}) \quad \frac{\langle E^1, A^1 \rangle \text{ main:pause} \xrightarrow{1} \langle E^1, A^1 \rangle \text{ main:copy}}{\langle E^1, A^1 \rangle \text{ main:weak abort}(a1, \{pause;\}) \xrightarrow{\perp} \langle E^1, A^1 \rangle \text{ main:copy}} \quad (A^1[a1] \neq 0)
$$

Step 4: Apply the (tick) and (copy) rules. The tick ends, the preemption statuses are reevaluated to $A^2$, and the program terminates.

$$
\begin{array}{l@{\qquad}l}
(\text{copy}) & \frac{\langle E^1, A^1 \rangle \text{ main:copy} \xrightarrow{0} \langle E^1, A^1 \rangle \text{ main:}}{\langle E^1, A^1 \rangle \text{ main:copy} \xrightarrow{0} \langle E^1, A^2 \rangle \text{ main:}} \\
(\text{tick}) &
\end{array}
$$
<figure><img src="image_31.png" /><figcaption>Fig. 29. Example of passing a shared variable by value and by reference.</figcaption></figure>

## C SHARED VARIABLES

This appendix describes how shared variables are passed by value or by reference into functions, and how the combine policies and combine functions work together to combine more than two copies of a shared variable. We compare the behaviors of the combine policies, all, new, and mod, using an illustrative example. We also provide additional examples of combine functions for primitive C data types and for programmer-specified data structures.

### C.1 Passing Shared Variables by Value and by Reference

Following the C convention, a function argument in ForeC can be passed by value or by reference. An argument passed by value can either be a shared or a private variable. For example, in Figure 29, line 4 makes a call to function *f* with the arguments *x* (a shared variable) and *y* (a private variable). The definition of function *f* (line 8) has parameters *d* (a private variable) and *e* (a shared variable) that are initialized with the values 3 (from *x*) and 5 (from *y*), respectively.

When passed by reference, the address of the function's argument is copied into the function's parameter. Thus, changes made to the dereferenced parameter are made to the argument. The following examples demonstrate how the shared type qualifier can be used in the declaration of references:

* `int* p` declares an ordinary C pointer to an `int` variable. This means that pointer `p` and the referenced `int` variable can only be accessed by at most one thread.

* `shared int* p` declares a pointer `p`, which can only be accessed by at most one thread, to a shared `int` variable. In Figure 29, line 11, the parameter of function `g` declares pointer `p` to a shared `int` variable. On line 5, the `&` unary operator is used to pass shared variable `x` into `g` by reference.

* `shared int shared* p` declares a shared pointer `p`, which can be accessed by multiple threads, to a shared `int` variable.

* `int shared* p` shorthand of `shared int shared* p` when only one thread can write to the referenced `int` variable.

### C.2 Combining More Than Two Copies

The ForeC program shown in Figure 30a is used to explain how multiple copies of a shared variable are combined. The program's control-flow graph is shown in Figure 30b. The program has a shared
<figure><img src="image_32.png" /></figure>

<figure><img src="image_33.png" /><figcaption>Fig. 30. Example ForeC program.</figcaption></figure>

variable called `s` that uses the combine function `plus`. The initial value of `s` is 3 for the program's first tick. Figure 31a shows the copies of `s` at the end of the first tick, organized by the thread genealogy. Each node represents a thread and the current value of its local copy, e.g., `main: 3` means that the main thread has a local copy of `s` with the value 3. Copies that were assigned a value during the tick have the `●` symbol, e.g., `tA: 1●` means that thread `tA`'s copy has been assigned the value 1. Arrows are drawn from the child threads to their parents to show the thread genealogy. Threads `tC` and `tD` create their copies from `tA`'s copy (see Section 2.5). Hence, the value of thread `tC`'s copy is 1. Threads `tE` and `tF` create their copies from `tB`'s copy.

The formal semantics of ForeC (Section 3) defines how more than two copies of a shared variable are combined. The copies from sibling threads (i.e., threads forked by the same `par` statement) are combined and the resulting value is assigned to their parent thread. Then, the copies of the parent and its sibling are combined together and assigned to their parent. This continues until the main thread is reached. Figure 31b illustrates the combine policy `all`, where all the copies are combined. The final combined value is 11 and it is assigned to shared variable `s` to complete the global tick.

The combine policy `new` only takes into account the copies for which the value has changed since the previous global tick. For the copies shown in Figure 31a, thread `main`, `tB`, and `tE`'s copies of `s` would be ignored. Although thread `tC` did not assign any value to its copy, the value was taken from thread `tA` who had assigned the new value 1 to its copy. Thus, thread `tC`'s copy does have a new value. Figure 31c illustrates the combine policy `new`. Note that thread `tF`'s copy is assigned directly to `tB` because its sibling's copy is ignored. The final combined value is 8.

For the combine policy `mod`, the copies that have not been assigned a value during the tick are ignored. For the copies shown in Figure 31a, thread `main`, `tB`, `tC`, and `tE`'s copies of `s` would be ignored. Figure 31d illustrates the combine policy `mod`. The final combined value is 7.
<figure><img src="image_34.png" /><figcaption>(a) The copies of s when tick 1 ends.</figcaption></figure>

<figure><img src="image_35.png" /><figcaption>(b) Policy all.</figcaption></figure>

<figure><img src="image_36.png" /><figcaption>(c) Policy new.</figcaption></figure>

<figure><img src="image_37.png" /><figcaption>(d) Policy mod.</figcaption></figure>

<caption>Fig. 31. Effects of the combine policies.</caption>

### C.3 Combine Policies Illustrated

This section illustrates the behavior of the combine policies all, new, and mod over several ticks by using the example of Figure 32. Figure 32a is a ForeC program that outputs the number of times that `button1` and `button2` were pressed in each tick. The program and its interface with the environment is illustrated in Figure 32b. On line 6 in Figure 32a, threads `t1` and `t2` are forked to check which buttons have been pressed. The results are assigned to the shared variable `count`. Line 6 also forks thread `t3` to read the value of `count` and to assign it to display output. Hence, three copies of `count` will be created in each tick. The copies of `count` are combined with the function `plus` (line 18) with the combine policy `mod`. Figure 33a provides possible input values for five ticks of the program. For example, only `button1` is pressed in tick 2. Figure 33b shows the value of the shared variable `count` and the value of each thread's local copy of `count`. The copies that were assigned a value during the tick have the `•` symbol. For tick 1, `count` is equal to 0; its initial value. From tick 2 onwards, the value of `count` corresponds to the number of button presses in the previous tick, because only threads `t1` and `t2`'s modified copies are combined.

Figure 33c illustrates the behavior of the combine policy `new` over several ticks. The values of threads `t1`, `t2`, and `t3`'s local copies are ignored when they have the same value as `count`. Figure 33d illustrates the behavior of the combine policy `all` over several ticks. In this case, threads `t1`, `t2`, and `t3`'s local copies are always used to compute the value of `count`. The value of `count` corresponds to the running total of button presses, i.e., in tick 6 a total of four button presses have occurred in previous ticks.
<figure><img src="image_38.png" /><figcaption>(a) ForeC program of the button counter.</figcaption></figure>

<figure><img src="image_39.png" /><figcaption>Fig. 32. Example of counting the number of button inputs.</figcaption></figure>

<figure><img src="image_40.png" /><figcaption>Fig. 33. The value of count under each combine policy.</figcaption></figure>
## C.4 Examples of Combine Functions

The simplest combine functions are those based on the associative and commutative binary mathematical operators:

* Arithmetic addition (+) and multiplication (*);

* Logical AND (&&) and OR (||);

* Bitwise AND (&) and OR (|);

* Minimum and maximum using if-else statement.

The combine functions should be associative and commutative so as to make the `par` statement associative (Lemma 13) and commutative (Lemma 15), relying only on the nesting of binary `par` statements to fork more than two child threads at the same time (e.g., `par(par(t₁, t₂), t₃) = par(t₁, par(t₂, t₃))`). The programmer is free to write combine functions based on non-associative or non-commutative binary operators (e.g., -, /, or %), but will negate the associative or commutative property, respectively, of the `par` statement.

Combine functions can also be defined for user-defined data structures. For example, Figure 34a defines a C-struct called `ProdSum` that stores the product (`prod`) and sum (`sum`) of the numbers assigned to it. The combine function `prodsum` multiplies all the values in `prod` and sums all the values in `sum`. An example of its behavior is provided after the function as comments.

For another example, Figure 34b defines a combine function that returns the minimum value that has been assigned since the start of the program. To achieve this, line 1 of Figure 34b defines a C-struct called `Min` that stores the value (`val`) that a thread assigns in the current tick and tracks the minimum value (`min`) that has been assigned since the start of the program. The combine function (line 3) stores in `res.val` the minimum value between `th1.val` and `th2.val`. Then, `res.min` stores the minimum value between itself and `res.val`.

The behavior of combine functions can be extended with dedicated threads that perform additional computations on the combined values of one or more shared variables. Figure 35 is an example ForeC program that calculates the average of three input values `in[i]`, declared on line 1 in Figure 35. Line 6 forks three threads `f` (line 9) to check the validity of each input. An input is valid if its value is greater than zero (line 11). In each tick, the threads assign valid inputs to their copy of the shared variable `val`. The modified copies of `val` are combined with the combine function `sum` (line 34), which sums the input values and the number of valid inputs. The average thread (line 22) reads the resulting combined value of `val` to calculate the average input value (line 29).
```c
1 typedef struct {int prod; int sum;} ProdSum;
2
3 ProdSum prodsum(ProdSum th1, ProdSum th2) {
4 ProdSum res = {.prod=(th1.prod*th2.prod), .sum=(th1.sum+th2.sum)};
5 return res;
6 }
7
8 // th1={.prod=2, .sum=2} and th2={.prod=5, .sum=5}
9 // prodsum(th1, th2)={.prod=10, .sum=7}
```

(a) Product and sum of two or more values.

```c
1 typedef struct {int val; int min;} Min;
2
3 Min min(Min th1, Min th2) {
4 Min res;
5 // Calculate the min for the current tick
6 if (th1.val>th2.val) {
7 res.val=th2.val;
8 } else {
9 res.val=th1.val;
}
10 // Calculate the min since the start of the program
11 if (th1.min>res.val) {
12 res.min res.val;
13 } else {
14 res.min=th1.min;
15 }
16
17 return res;
18 }
19
20 // Initial value: res={.value=0, .min=0}
21 //
22 // Tick 1:
23 // th1={.value=1, .min=0} and th2={.value=2, .min=0}
24 // min(th1, th2)={.value=1, .min=0}
25 //
26 // Tick 2:
27 // th1={.value=-1, .min=0} and th2={.value=2, .min=0}
28 // min(th1, th2)={.value=-1, .min=-1}
```

(b) Minimum of two or more values.

<caption>Fig. 34. Examples of combine functions for C-structs.</caption>
<figure><img src="image_41.png" /><figcaption>Fig. 35. Averaging two or more values.</figcaption></figure>
Received 25 March 2022; revised 13 January 2023; accepted 8 March 2023