Asynchronous Programming in a Prioritized Form
Mohamed A. El-Zawawy1,2
of Computer and Information Sciences
Al Imam Mohammad Ibn Saud Islamic University
Riyadh, Kingdom of Saudi Arabia

arXiv:1501.00669v1 [] 4 Jan 2015

1 College

2 Department

of Mathematics
Faculty of Science
Cairo University
Giza 12613, Egypt
maelzawawy@cu.edu.eg

Abstract: Asynchronous programming has appeared as a programming style that overcomes undesired properties
of concurrent programming. Typically in asynchronous models of programming, methods are posted into a post
list for latter execution. The order of method executions is serial, but nondeterministic.
This paper presents a new and simple, yet powerful, model for asynchronous programming. The proposed model
consists of two components; a context-free grammar and an operational semantics. The model is supported by
the ability to express important applications. An advantage of our model over related work is that the model simplifies the way posted methods are assigned priorities. Another advantage is that the operational semantics uses
the simple concept of singly linked list to simulate the prioritized process of methods posting and execution. The
simplicity and expressiveness make it relatively easy for analysis algorithms to disclose the otherwise un-captured
programming bugs in asynchronous programs.
Key–Words: Prioritized posting, asynchronous programming, operational semantics, context-free grammar, concurrent programming.

1 Introduction
All contemporary appliances (mobile, desktop, or
web applications) require high responsiveness which
is conveniently provided by asynchronous programming. Hence application program interfaces (APIs)
enabling asynchronous, non-blocking tasks, such as
web access or file operations) are accommodated
in dominant programming languages. APIs provide
asynchronous programming but mostly in a hard way.
For example consider the following situation. A
unique user interface (UI) task thread is typically used
to design and implement user interfaces. Hence events
on that thread simulate tasks that change the UI state.
Therefore when the UI cannot be redrawn or respond,
it get freezed. This makes it sensible, in order to keep
the application responding continuously to UI tasks,
to run blocking I/O commands and long-lasting CPUbound asynchronously.
Asynchronous programming has multi-threaded
roots. This is so as APIs have been implemented using
multi-threaded programs with shared-memory. Software threads execution is not affected by the number
of processors in the system. This is justified by the

fact that the threads are executed as recursive sequential softwares running concurrently with interleaved
write and reads commands. The many possible interleavings in this case cause the complexity of models
of concurrent programming [8]. In a complex process,
atomic locking commands can be added for prevention and prediction of bad thread interleavings. The
non-deterministic style of interleaving occurrence creates rarely appearing programming-errors which are
typically very hard to simulate and fix. This difficulty lead researchers to design multi-threaded programs (of APIs) in the framework of asynchronous
programming models [6, 7].
The relative simplicity of asynchronous programming makes it a convenient choice to implement APIs
or reactive systems. This is proved by recent years intense use of asynchronous programming by servers,
desktop applications, and embedded systems. The
idea of asynchronous programming is to divide cumulative program executions into tasks that are brieflyrunning. Moreover accessing the shared memory,
each task is executed as a recursive sequential software that specifies (posts) new methods to be executed
later.

Many attempts were made to present formal asynchronous programming models. However few attempts [5] were made to express and formalize the
fact that posted tasks in asynchronous programs may
well have different execution priorities. A big disadvantage of existing work [5] that considers execution
priorities is the complexity of the models hosting such
priorities. For example the work in [5] considers the
execution priorities using several task-buffers which
makes the solution a bit involved.
This paper presents a simple, yet powerful, model
for asynchronous programming with priorities for task
posting. We call the proposed model AsynchP . The
paper also presents a novel and robust operational semantics for the constructs of AsynchP . A simple
singly linked list of prioritized posted tasks is used to
precisely capture the posting process. Our proposed
asynchronous model is to simplify analyzing asynchronous programs [4].

Motivating Example
A motivating example of designing our model comes
form the way hardware interactions take place in operating systems (more specifically in Windows) kernels.
Concepts of prioritized interrupt sets are used to simulate these hardware interactions in an asynchronous
style. For such applications a simple, yet powerful
and mathematically well founded, model for prioritized asynchronous programming is required.

Contribution
The contributions of this paper are:

2 Prioritized Asynchronous
gramming Model

Pro-

This section presents our model, AsynchP , for prioritized asynchronous programming. In AsynchP , each
posted method has an execution priority. An asynchronous program execution is typically divided into
quick-running methods (tasks). Tasks of higher priority get executed first and task of equal priorities are
executed using the first come first serviced strategy.
Asynchronous programming has an important application in reactive systems where a single task must
not be allowed to run too long and to prevent executing other (potentially) highly prioritized tasks.
Figure 1 presents the simple and powerful model
AsynchP for prioritized asynchronous programming.
Considering single local and global variables and using free syntax of expressions does not cause any generality lose. However each expression is built using
the global variable of the program and the local variable of the active method. A AsynchP program P
consists of a single global variable g and a sequence
of methods denoted M1 , . . . , Mn . The Provided(e)
statement continues executing the program provided
that the expression e evaluates to a non-zero value.
Each method M is expressed as a structure
meth(m, l, S) of a method name, a single local variable l, and a top-level statement S. The sets of all program methods and statements are denoted by Meths
and Stmts, respectively. Intuitively, the asynchronous
call is modeled by the statement Synch(m(e),p)
where:
• the called method name is m,
• the calling parameter is the expression e, and
• the execution priority of this call is p.

• A prioritized asynchronous programming model;
AsynchP .
• A novel operational semantics for AsynchP programs.

Organization
The rest of the paper is organized as follows. Section 2
presents the proposed prioritized asynchronous programming model – AsynchP . The semantics of prioritized asynchronous programming model; AsynchP
is shown in Section 3 which is followed by Section 4
that reviews related work and presents directions for
future work. The last section (Section 5) of the paper
concludes it.

We assume three levels of execution priorities;
{high(1), medium(2), low(3)}.

3 Mathematical
AsynchP

Framework

for

This section presents a novel operational semantics
for asynchronous programs built using AsynchP . Our
semantics is based on a singly liked-list (which we call
Asynchronous Linked List (ALL)) to host the posted
methods. ALL is divided into three regions using
pointers. The first, the middle, and last regions of ALL
host posted methods that have high, medium, and low
execution priorities, respectively.
Definition 1 introduces formally the concept of
(Asynchronous Node (AN)) to be used to build ALL.

g ∈ G = Global variable names.
l ∈ L = Method local variable names.
p ∈ P = {high(1), medium(2), low(3)}
= The set of all synchronization priorities.
m ∈ M = The set of all method names.
v ∈ V al = the set of possible values of local and global variables.
S ∈ Stats

::=

S1 ; S2 | g := e | l := e | Provided e | if e then St else Sf |
while e do S | run m(e) | return() | Synch(m(e),p).

M ∈ Meths

::=

meth(m, l, S).

P ∈ Programs

::=

program(g, M ∗ ).

Figure 1: AsynchP : a language model for a simple prioritized asynchronous programming.
Definition 1 An asynchronous node (AN), n, is a single linked list node whose data contents are two locations containing:
• x1 : a method name, and
• x2 : a parameter expression.
For a method call m(e) in a AsynchP program, we let
Nodem(e) denotes the asynchronous node whose locations x1 and x2 contain m and e, respectively. The
set of all asynchronous nodes is denoted by NodesA .
Definition 2 introduces formally the concept of
Asynchronous Linked List (ALL) that is to be used to
accurately capturing the semantics of the constructs of
the proposed asynchronous model.
Definition 2 An asynchronous linked list (ALL),
li =< f, c, eh , em >,

(1)

is a singly linked list whose nodes are asynchronous
nodes (in NodesA ) such that:
• f is a pointer to the first node of the list,
• c is a pointer to the current node, and
• eh , em are pointers to the last node in the list
hosting a method of high and medium priorities,
respectively.
The set of all asynchronous linked lists is denoted by
ListsA .
Whenever a method gets posted, an asynchronous
node is created and inserted into an asynchronous list.
If the posted method is of priority h or m, the created node gets inserted after the nodes pointed to by
eh or em , respectively. If the posted method is of priority l, the created node gets inserted at the end of the

list. Whenever a posted method is to be executed, the
method corresponding to the head of an asynchronous
node is executed and that head gets removed form the
list. These two operations are assumed to be carried
out by the functions defined in Definition 3.
Definition 3 Let li =< f, c, eh , em > be a asynchronous linked list (in ListsA ). We let
• addA : NodesA ×P ×ListsA → ListsA denotes a
map that adds a given node n of a given priority
p after the node pointed to be li.ep in a given list
li1 .
• removeA : ListsA → NodesA × ListsA denotes
a map that removes the first node of a given list
li and return the removed node and the resulting
linked list.
Definition 4 introduces the states of our proposed
operational semantics.
Definition 4 Let program(g, M1 , . . . , Mn ), where
Mi = meth(mi , li , Si ), be a program in AsynchP . An
asynchronous program state (APS) is a triple (s,li,sk),
where:
• s is a partial map from G ∪ (M × L) to Val.
• li is an asynchronous linked list.
• sk is stack of method names.
We let Mi .l and Mi .l denote li and Si , respectively.
Each semantic state is a triple of a partial map captures
the contents of global and local variables, an asynchronous linked list, and a stack of method names.
1

list

Note that p ∈ {h, m, l}. If p = l, el is the last node in the

li′ = addA (Node(m(e)), p, li)
Synch(m(e), p)) : (s, li, sk) → (s, li′ , sk)
is-empty(sk) = false

sk′ = pop(sk)

return() : (s, li, sk) → (s, li, sk′ )

(synchs )

(returns )

m′ = peek(sk)
v = ke(s(g), s(m′ .l)k
s′′ = s[m.l 7→ v]
′′
′′
′′
sk = push(sk, m)
m.S : (s , li, sk ) → (s′ , li′ , sk′ )
(runs )
run m(e) : (s, li, sk) → (s′ , li′ , sk′ )
m′ = peek(sk)

v = ke(s.g, m′ .l)k

g := e : (s, li, sk) → (s[g 7→ v], li, sk)
m′ = peek(sk)

(:=sg )

v = ke(s.g, m′ .l)k

l := e : (s, li, sk) → (s[m′ .l 7→ v], li, sk)
m′ = peek(sk)

ke(s.g, m′ .l)k =
6 0

(:=sl )

(ps )

Provided e : (s, li, sk) → (s, li, sk)
m′ = peek(sk)

ke(s.g, m′ .l)k = 0

(w1s )

while e do S : (s, li, sk) → (s, li, sk)
m′ = peek(sk)
ke(s.g, m′ .l)k =
6 0
S : (s, li, sk) → (s′′ , li′′ , sk′′ )
while e do S : (s′′ , li′′ , sk′′ ) → (s′ , li′ , sk′ ) (ws )
2
while e do S : (s, li, sk) → (s′ , li′ , sk′ )
m′ = peek(sk)
ke(s.g, m′ .l)k = 0
Sf : (s, li, sk) → (s′ , li′ , sk′ )
(ifs1 )
if e then St else Sf : (s, li, sk) → (s′ , li′ , sk′ )
m′ = peek(sk)
ke(s.g, m′ .l)k =
6 0
′
St : (s, li, sk) → (s , li′ , sk′ )
(ifs2 )
if e then St else Sf : (s, li, sk) → (s′ , li′ , sk′ )
S1 : (s, li, sk) → (s′′ , li′′ , sk′′ )

S2 : (s′′ , li′′ , sk′′ ) → (s′ , li′ , sk′ )
′

′

′

(;s )

S1 ; S2 : (s, li, sk) → (s , li , sk )

Figure 2: Transition rules for statements.
The stack is meant to keep the order in which methods
call each other.
Figures 2 and 3 present the transition rules of the
proposed operational semantics. Some comments on
the rules are in order. The rule synchs creates an asynchronous node corresponding to the method m and the
parameter e. Using the map addA , the node then is
added to the asynchronous list li to get the new list li′ .
The rule (returns ), pops an element from the method
stack as the return statement means that the top element of the stack is executed. The rule (runs ) first
peeks the first element of the stack to get the local variable (m′ .l) of the currently active method. This local
variable is then used together with the global variable
to evaluate the expression e. The resulting value is
used to modify the local variable of the method (m)
that is to be executed. Then m is pushed into the stack
and the statement of m is executed.

The rule (progs ) first runs the statements of all
methods of the program being executed then runs all
statements of the methods that is posted. The posted
statements are executed via the rules (⇒s1 ) and (⇒s2 ).

4 Related and Future Work
Parallel, distributed, reactive, and concurrent programming have been attracting much researcher activities. The asynchronous programming methodologies
include:
• multi-threaded light-weight orchestration programming [19],
• thread Join-based allocation,
• typed synchronous programming languages [20],
• functional sensible programming,

(⇒s1 )
(s, empty, empty) ⇒ (s, empty, empty)
(n, li′ ) = removeA (li)
n.x1 .S : (s, li′ , empty) → (s′′ , li′′ , empty)
(s′′ , li′′ , empty) ⇒ (s′ , empty, empty)
(⇒s2 )
(s, li, empty) ⇒ (s′ , empty, empty)
sk′′ = push(m, sk)

S : (s, li, sk′′ ) → (s′ , li′ , sk′ )

meth(m, l, S) : (s, li, sk) → (s′ , li′ , sk′ )

(meths )

∀1 ≤ i ≤ n. Mi : (si , lii , ski ) → (si+1 , lii+1 , ski+1 )
(sn+1 , lin+1 , empty) ⇒ (s′ , empty, empty)
(progs )
program(g, M1 , . . . , Mn ) : (s1 , li1 , sk1 ) → (s′ , empty, empty)

Figure 3: Transition rules for methods and programs.
• promises, and
• co-methods and futures agents [21, 22].
Event-based techniques for programming have been
using continuations which are delimited monadic [17,
18]. Fork-join, task, async, and event functions appear
not to rely on a specific language design. There is
a big research debate about the relationship between
threads and events in systems research [16].
In an asynchronous program, executions containing context switches bounded by a user-specified limit
are explored by context-bounded verification [14, 15].
This context-bounding idea is not reasonable for programs with big number of events. Several treatments
for this problem have been proposed for this problem. Without losing decidability, [13] proposed a
context-minimizing technique permitting unbounded
context switches. For asynchronous concurrent programs, in [12], the round-robin technique for scheduling is used to enable unbounded context switches.
Sequential techniques are also used to analyze
asynchronous programs. In [14], a source-to-source
technique building sequential programs from multithreaded programs was proposed via under approximating the possible set of executions of the input program. A novel source-to-source transformation providing for any context-bound, a context-bounded under approximation was presented in [11]. A main
issue of the work in [11] is that the resulting sequential program may host main states unreachable
in the given asynchronous program. Other techniques
like [10] treat this problem by repeatedly running the
code to the control points where used-defined valued are needed. The work in [9] compares the techniques of asynchronous programs verifications that
use verification-condition-checking against that use
model-checking. One major results of this work is that
eager approaches outperforms lazy ones. The work
in [8] uses the construction using a bound on the task

number, to reduce asynchronous programs into sequential programs via priority-preemptive schedulers.
The work presented in this paper is close to sequentialization [14]; the concept describing compositional reductions to get sequential programs from concurrent ones. Although sequentialization started by
checking multi-threaded programs with one contextswitch, it was developed later to treat a user-specified
number of context-switches. These switches occur
among statically-specified group of threads running
using RR order [11]. In [2], a technique for treating context switches among an unspecified number of
dynamically-created tasks was presented. This technique (in [2]) hence explicitly treats event-oriented
asynchronous programs.
For future work, it is interesting to devise static
analyses for asynchronous programs using the model
AsynchP [1]. Initial experiments show that our proposed model is expected to support devising robust
and powerful analysis techniques. An examples of
targeted analyses is dead-posting elimination which
aims at removing the unnecessary posting statements
from asynchronous programs.

5 Conclusion
Main reason to use asynchronous programming is
to overcome some problems of concurrent programming. The main idea of asynchronous programming
is to post methods into a post list for latter execution.
The order of executing these methods is nondeterministically serial.
A new and simple, yet powerful, model for asynchronous programming was presented in this paper. More precisely, the paper proposed a contextfree grammar and an operational semantics for asynchronous programming. One important aspect of the
proposed model is supporting posting methods with

execution priorities.
[10]
References:
[1] El-Zawawy, M.A.: Detection of probabilistic
dangling references in multi-core programs using proof-supported tools. In: Murgante, B.,
Misra, S., Carlini, M., Torre, C.M., Nguyen, H.Q., Taniar, D., Apduhan, B.O., Gervasi, O. (eds.)
ICCSA 2013, Part V. LNCS, vol. 7975, Springer,
Heidelberg (2013), pp. 516–530.
[2] M. Emmi, S. Qadeer, and Z. Rakamaric. Delaybounded scheduling. In POPL 11: Proc. 38th
ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, ACM, 2011,
pp. 411–422.
[3] N. Kidd, S. Jagannathan, and J. Vitek. One stack
to run them all: Reducing concurrent analysis
to sequential analysis under priority scheduling.
In SPIN 10: Proc. 17th International Workshop
on Model Checking Software, volume 6349 of
LNCS, Springer, 2010, pp. 245–261.
[4] M. F. Atig, A. Bouajjani, and T. Touili. Analyzing asynchronous programs with preemption. In
FSTTCS 08: Proc. IARCS Annual Conference
on Foundations of Software Technology and Theoretical Computer Science, volume 2 of LIPIcs,
Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2008, pp. 37–48.
[5] Michael Emmi, Akash Lal, Shaz Qadeer: Asynchronous programs with prioritized task-buffers.
SIGSOFT FSE 2012,48.
[6] K. Sen and M. Viswanathan. Model checking multithreaded programs with asynchronous
atomic methods. In CAV 06: Proc. 18th International Conference on Computer Aided Verification, volume 4144 of LNCS, Springer,
2006,pp. 300–314.
[7] R. Jhala and R. Majumdar. Interprocedural analysis of asynchronous programs. In POPL 07:
Proc. 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages,
ACM, 2007, pp. 339–350.
[8] N. Kidd, S. Jagannathan, and J. Vitek. One stack
to run them all: Reducing concurrent analysis
to sequential analysis under priority scheduling.
In SPIN ’10: Proc. 17th International Workshop
on Model Check- ing Software, volume 6349 of
LNCS, Springer, 2010, pp. 245–261.
[9] N. Ghafari, A. J. Hu, and Z. Rakamarifc. Contextbounded translations for concurrent software: An empirical evaluation. In SPIN ’10:
Proc. 17th Interna- tional Workshop on Model

[11]

[12]

[13]

[14]

[15]

[16]

[17]

[18]

[19]

[20]

Checking Software, volume 6349 of LNCS,
Springer, 2010, pp. 227–244.
S. La Torre, P. Madhusudan, and G. Parlato. Reducing context-bounded concurrent reachability
to sequential reachability. In CAV ’09: Proc. 21st
International Conference on Computer Aided
Verification, volume 5643 of LNCS, Springer,
2009, pp. 477–492.
A. Lal and T. W. Reps. Reducing concurrent
analysis under a context bound to sequential
analysis. Formal Methods in System Design,
35(1), 2009, pp. 73–97.
S. La Torre, P. Madhusudan, and G. Parlato. Modelchecking parameterized concurrent
programs using linear interfaces. In CAV ’10:
Proc. 22nd International Conference on Computer Aided Verification, volume 6174 of LNCS,
Springer, 2010, pp. 629–644.
M. F. Atig, A. Bouajjani, and S. Qadeer. Contextbounded analysis for concurrent programs
with dynamic creation of threads. In TACAS ’09:
Proc. 15th International Conference on Tools
and Algorithms for the Construction and Analysis of Systems, volume 5505 of LNCS, Springer,
2009, pp. 107–123.
S. Qadeer and D.Wu. KISS: Keep it simple and
sequential. In PLDI ’04: Proc. ACM SIGPLAN
Conference on Programming Language Design
and Implementation, ACM, 2004, pp. 14–24.
S. Qadeer and J. Rehof. Context-bounded model
checking of concurrent software. In TACAS ’05:
Proc. 11th International Conference on Tools
and Algorithms for the Construction and Analysis of Systems, volume 3440 of LNCS, Springer,
2005, pp 93–107.
G. Kerneis, J. Chroboczek, ContinuationPassing C, compiling threads to events through
continuations, Higher-Order and Symbolic
Computation (LISP), 24(3), 2011, pp. 239–279.
A. Holzer, L. Ziarek, K. Jayaram, P Eugster,
Putting events in context: aspects for eventbased distributed programming, AOSD, 2011,
pp. 241–252.
L. Vaseux, F. Otero, T. Castle, C. Johnson,
Event-based graphical monitoring in the
EpochX genetic programming framework,
GECCO (Companion), 2013, pp. 1309–1316.
R. Ranjan, B. Benatallah, Programming Cloud
Resource Orchestration Framework: Operations
and Research Challenges, CoRR abs/1204, 2204
,2012.
J. Aguado, M. Mendler, R. Hanxleden,
I. Fuhrmann, Grounding Synchronous Deterministic Concurrency in Sequential Programming. ESOP, 2014, pp. 229–248.

[21] G. Gori, E. Johnsen, R. Schlatte, V. Stolz,
Erlang-Style Error Recovery for Concurrent Objects with Cooperative Scheduling. ISoLA, 2014,
pp. 5–21.
[22] J. Nelson, Co-ops: concurrent algorithmic skeletons for Erlang. Erlang Workshop, 2012, pp. 61–
62.

