A Concurrent Model for Imperative Languages with Improved Atomicity

TL;DR

This paper introduces a new concurrent programming model with block sequential statements that execute code blocks atomically, improving atomicity and predictability in imperative languages, exemplified by an extension of concurrent C.

Contribution

It presents a novel concurrent model featuring block sequential statements for atomic execution, enhancing control and predictability in imperative languages.

Findings

Introduces block sequential statement for atomic execution.

Extends concurrent C with new atomicity features.

Improves atomicity and predictability in concurrent programming.

Abstract

We propose a new concurrent model for imperative languages where concurrency occurs at a subprogram level. This model introduces a new {\it block sequential} statement of the form $#(G_1,\ldots,G_n)$ where each $G_i$ is a statement. This statement tells the machine to execute $G_1,\ldots,G_n$ sequentially and atomically (\ie, without interleaving). It therefore enhances atomicity and predictability in concurrent programming. We illustrate our idea via $C^{\|}$, an extension of the core concurrent C with the new block sequential statement.

Full text

{summary}

We propose a new concurrent model for imperative languages where concurrency occurs at a subprogram level. This model introduces a new block sequential statement of the form $\sharp(G_{1},\ldots,G_{n})$ where each $G_{i}$ is a statement. This statement tells the machine to execute $G_{1},\ldots,G_{n}$ sequentially and atomically (i.e., without interleaving). It therefore enhances atomicity and predictability in concurrent programming.

We illustrate our idea via C*∥*, an extension of the core concurrent C with the new block sequential statement.

1 Introduction

Adding concurrency to imperative programming – C, its extension [6] and Java – is an attractive task. While concurrent programming may appear to be a simple task, it has proven too difficult to use, predict or debug.

An analysis shows that this difficulty comes from the fact that interleavings among threads – which are typically done by OS schedulers – are quite arbitrary and cannot be controlled at all by the programmer.

We observe that concurrent programming can be made easier by making interleaving less arbitrary and more controlled. Inspired by [4, 5], we propose two ideas for this. First, we propose a concurrent model with its own embedded scheduler. Our scheduler works on a high-level: it allows the execution to switch from one assigment statement to another. This is in contrast to OS schedulers which allows the execution to switch from one machine instruction to another. For example, the assignment statement $c=c+1$ is $atomic$ in the sense that it runs to completion without being interleaved. This reduces nondeterminism and error known as transient errors.

Second, semaphores and monitors are typically used as facilities for mutual exclusion. We propose a simpler method to solve mutual exclusion. Toward this end, we propose a new block sequential statement $\sharp(G_{1},\ldots,G_{n})$, where each $G_{i}$ is a statement. This has the following execution semantics: execute $G_{1},\ldots,G_{n}$ sequentially and consecutively (i.e., without being interleaved). In other words, our interpreter treats $\sharp(G_{1},\ldots,G_{n})$ atomic. This can be easily implemented by designing our interpreter working in two different modes: the $concurrent$ mode and the traditional $sequential$ mode. Thus, if our interpreter encounters $\sharp(G_{1},\ldots,G_{n})$, it switches from the concurrent mode to the sequential mode and proceeds just like the traditional C interpreter. In this way, atomicity of this statement is guaranteed. We intend to use this construct to each critical region.

This paper focuses on the minimum core of C, enhanced with concurrency at a subprogram level. This is to present the idea as concisely as possible. The remainder of this paper is structured as follows. We describe C*∥, an extension of concurrent C with a new statement in Section 2. In Section 3, we present an example of C∥*. Section 4 concludes the paper.

2 The Language

The language is core C with procedure definitions. It is described by $G$- and $D$-formulas given by the syntax rules below:

[TABLE]

In the above, $A$ represents a head of an atomic procedure definition of the form $p(x_{1},\ldots,x_{n})$ where $x_{1},\ldots,x_{n}$ are parameters. A $D$-formula is called a procedure definition. In the transition system to be considered, a $G$-formula will function as a thread and a set of $G$-formulas (i.e., a set of threads) will function as the main statement, and a set of $D$-formulas enhanced with the machine state (a set of variable-value bindings) will constitute a program. Thus, a program is a union of two disjoint sets, i.e., $\{D_{1},\ldots,D_{n}\}\cup\theta$ where each $D_{i}$ is a $D$-formula and $\theta$ represents the machine state. Note that $\theta$ is initially set to an empty set and will be updated dynamically during execution via the assignment statements.

We will present an interpreter for our language via a proof theory [3, 8, 7, 9]. This is in contrast to other complex approaches to describing an interpreter for concurrent languages [1, 2]. Note that our interpreter alternates between the concurrent execution phase and the backchaining phase. In the concurrent execution phase (denoted by $ex({\cal P},\|(\Gamma,G,\Delta),{\cal P}^{\prime})$) it tries to select and execute a thread $G$ among a set of threads ($\Gamma,G,\Delta$) with respect to a program ${\cal P}$ and produce a new program ${\cal P}^{\prime}$ by reducing $G$ to simpler forms until $G$ becomes an assignment statement, true or a procedure call. The rules (4)-(11) deal with this phase. Here both $\Gamma$ and $\Delta$ denote a set of $G$-formulas. If $G$ becomes a procedure call, the interpreter switches to the backchaining mode. This is encoded in the rule (3). In the backchaining mode (denoted by $bc(D,{\cal P},A,{\cal P}^{\prime},\Gamma,\Delta)$), the interpreter tries to solve a procedure call $A$ and produce a new program ${\cal P}^{\prime}$ by first reducing a procedure definition $D$ in a program ${\cal P}$ to its instance (via rule (2)) and then backchaining on the resulting definition (via rule (1)). To be specific, the rule (2) basically deals with argument passing: it eliminates the universal quantifier $x$ in $\forall xD$ by picking a value $t$ for $x$ so that the resulting instantiation, written as $[t/x]D$, matches the procedure call $A$. The notation $S$ seqand $R$ denotes the sequential execution of two tasks. To be precise, it denotes the following: execute $S$ and execute $R$ sequentially. It is considered a success if both executions succeed. Similarly, the notation $S$ parand $R$ denotes the parallel execution of two tasks. To be precise, it denotes the following: execute $S$ and execute $R$ in any order. Thus, the execution order is not important here. It is considered a success if both executions succeed. The notation $S\leftarrow R$ denotes reverse implication, i.e., $R\rightarrow S$.

Definition 1**.**

Let $\|(G_{1},\ldots,G_{n})$ be a sequence of threads to run concurrently and let ${\cal P}$ be a program. Then the notion of executing $\langle{\cal P},\|(G_{1},\ldots,G_{n})\rangle$ concurrently and producing a new program ${\cal P}^{\prime}$– $ex({\cal P},\|(G_{1},\ldots,G_{n}),{\cal P}^{\prime})$ – is defined as follows:

• (1) 

$bc((A=G_{1}),{\cal P},A,{\cal P}_{1},\Gamma,\Delta)\ \leftarrow$* *

$ex({\cal P},\|(\Gamma,G_{1},\Delta),{\cal P}_{1})$. % A matching procedure for $A$ is found.

• (2) 

$bc(\forall xD,{\cal P},A,{\cal P}_{1},\Gamma,\Delta)\ \leftarrow$* *

$bc([t/x]D,{\cal P},A,{\cal P}_{1},\Gamma,\Delta)$. % argument passing

• (3) 

$ex({\cal P},\|(\Gamma,A,\Delta),{\cal P}_{1})\ \leftarrow$* $(D\in{\cal P}$ parand $bc(D,{\cal P},A,{\cal P}_{1},\Gamma,\Delta))$. % $A$ is a procedure call*

• (4) 

$ex({\cal P},\|(true),{\cal P})$. % True is always a success.

• (5) 

$ex({\cal P},\|(),{\cal P})$. % Empty threads mean a success.

• (6) 

$ex({\cal P},\|(\Gamma,x=E,\Delta),{\cal P}_{1})\ \leftarrow$* *

$eval({\cal P},E,E^{\prime})$* seqand % evaluate $E$ to get $E^{\prime}$ *

$(ex({\cal P}\uplus\{\langle x,E^{\prime}\rangle\},\|(\Gamma,\Delta),{\cal P}_{1})$**

% If an assignment statement $x=E$ is chosen by our interpreter, update $x$ to $E^{\prime}$ and return to the interpreter. Here, $\uplus$ denotes a set union but $\langle x,V\rangle$ in ${\cal P}$ will be replaced by $\langle x,E^{\prime}\rangle$.

• (7) 

$ex({\cal P},\|(\Gamma,;(),\Delta),{\cal P}_{1})\ \leftarrow$* *

$ex({\cal P},\|(\Gamma,\Delta),{\cal P}_{1}))$. % an empty sequential composition is a success.

• (8) 

$ex({\cal P},\|(\Gamma,;(G_{1},\ldots,G_{m}),\Delta),{\cal P}_{2})\ \leftarrow$* *

$(ex({\cal P},\|(G_{1}),{\cal P}_{1})$* seqand *

$ex({\cal P}_{1},\|(\Gamma,;(G_{2},\ldots,G_{m}),\Delta),{\cal P}_{2}))$. %

% If a sequential composition $;(G_{1},\ldots,G_{m})$ is chosen, execute $G_{1}$ in sequential mode and then return to the interpreter with the rest.

• (9) 

$ex({\cal P},\|(\Gamma,repeat(G),\Delta),{\cal P}_{2})\ \leftarrow$* *

$(ex({\cal P},\|(G),{\cal P}_{1})$* seqand *

$ex({\cal P}_{1},\|(\Gamma,repeat(G),\Delta),{\cal P}_{2}))$.

% If a repeat statement $repeat(G)$ is chosen, execute $G$ in sequential mode and then return to the interpreter with the rest plus $repeat(G)$.

• (10) 

$ex({\cal P},\|(\sharp()),{\cal P})$*. *

% An empty block sequential statement is a success.

• (11) 

$ex({\cal P},\|(\Gamma,\sharp(G_{1},\ldots,G_{m}),\Delta),{\cal P}_{3})\ \leftarrow$* *

$(ex({\cal P},\|(G_{1}),{\cal P}_{1})$* seqand *

$(ex({\cal P}_{1},\|(\sharp(G_{2},\ldots,G_{m})),{\cal P}_{2})$* seqand *

$ex({\cal P}_{2},\|(\Gamma,\Delta),{\cal P}_{3}))$.

*% If a block sequential statement $\sharp(G_{1},\ldots,G_{m})$ is chosen, execute $G_{1}$ in sequential mode and then $\sharp(G_{2},\ldots,G_{m})$ in sequential mode and then return to the interpreter (which proceeds in concurrent mode) with the remaining. *

If $ex({\cal P},G,{\cal P}_{1})$ has no derivation, then the interpreter returns the failure. Initially it works in the concurrent mode. In the concurrent mode, we assume that our interpreter chooses a thread using some predetermined algorithm. Note that executing $one$ thread $G$ concurrently, denoted by $\|(G)$, is identical to executing $G$ sequentially.

3 Examples

As a well-known example, we examine the system that allows people to sign up for a mailing list. An example of this class is provided by the following code where the procedure below adds a person to a list:

[TABLE]

and the main program consists of two concurrent threads as follows:

[TABLE]

In the above, we used a more traditional notation $(G_{1}\sharp,\ldots,\sharp G_{n})$ instead of $\sharp(G_{1},\ldots,G_{n})$.

Although the above signup procedure is in fact a critical section, it works correctly because no interleaving – due to the presence of $\sharp$ –is allowed in the critical section. Note that our code is very concise compared to the traditional ones using semaphores.

4 Conclusion

In this paper, we proposed a simple concurrent model for imperative languages. This model introduces a block sequential statement $\sharp(G_{1},\ldots,G_{n})$ where each $G_{i}$ is a statement. This statement executes $G_{1},\ldots,G_{n}$ sequentially and atomically. It therefore enhances atomicity and predictability.

Although we focused on a simple concurrent model for imperative language at a subprogram level, it seems possible to apply our ideas to existing concurrent and parallel computing models [1, 2].

5 Acknowledgements

This work was supported by Dong-A University Research Fund.