Towards Concurrent Program¶
The type system of ATS consists of both dependent types and linear types. Please refer to ATS’ documentation for its application in constructing verifiably correct sequential progarm. Linear types are of help to certain extent in ensuring safety properties about mutual exclusion. However, in general, the type system of ATS has difficulty in specifying properties of concurrent programs, e.g. invariants of objects across threads, absence of deadlock, liveness properties, and etc. Such incapability triggers our research in corporating model checking techniques into the verification process of ATS program.
Primitives for Concurrent Programming¶
But first of all, programmers have to be able to write concurrent programs in ATS. Currently, we add a set of primitives into ATS programming language to support concurrent programming in a style similar to using pthead. In the near future, we will add more primitives (e.g. channel, future) supporting different styles of concurrent programming.
The declarations of these primitives can be found in conats.sats
. In the
Tutorial, we already use conats_shared_create, conats_shared_acquire,
conats_shared_condwait, conats_shared_signal, and conats_shared_release, whose
types are declared as follows:
1 2 3 4 5 6 7 8 9 10 | abstype shared_t (viewt@ype, int)
typedef shared (a:viewt@ype) = shared_t (a, 1)
fun conats_shared_create {a: viewt@ype} (ele: a): shared (a)
fun conats_shared_acquire {a: viewt@ype} {n:pos} (s: shared_t (a, n)): a
fun conats_shared_release {a: viewt@ype} {n:pos} (s: shared_t (a, n), ele: a): void
fun conats_shared_signal {a: viewt@ype} (s: shared (a), ele: a): a
fun conats_shared_condwait {a: viewt@ype} (s: shared (a), ele: a): a
|
conats_shared_create creates a shared object (of type shared a) holding a linear buffer. The concept of shared object is similar to that of monitor [1]. The types of the aforementioned functions guarantee they are invoked appropriately in a non-object-oriented language like ATS. (E.g. we have to call conats_shared_acquire before invoking conats_shared_condwait and conats_shared_signal. From the perspective of pthread programming, a shared object consists of a mutex and a condition variable working together for synchronization purpose.
However, sometimes it’s not enough for a shared object to contain just one condition
varialbe. For example, in Tutorial, the shared object has only one
condition varialbe, which is used to indicate two situations: buffer is full or
empty. The example has no deadlock because it only has one producer and one consumer.
Simply adding one more consumer to the example would lead to potential deadlock. The
complete code can be downloaded here 16_1_producer_consumer_m_1.dats
. You can also find this example at our website Model Checking ATS.
One example of the potential deadlock can be thought as follows: Initially, the
shared buffer is empty. Two consumers come and wait on the shared object. The
producer comes and puts one element into the buffer and then wake up one consumer.
However, the newly active consumer doesn’t execute instantly. Instead, the
producer comes again, tries to put another element into the buffer, and has to wait
on the shared object since the capacity of the buffer is 1. Then the newly active
consumer gets one element out of the buffer and wakes up another consumer. At this
moment, the buffer is empty, the producer is waiting, and two consumers won’t signal
the shared buffer any more. And this leads to a deadlock. The counterexample found by
the model checker by Breadth First Search confirms with our speculation.
To solve this problem, we also provide another version of shared object which contains multiple condition variables. The types of related functions are shown below.
1 2 3 4 5 6 7 | abstype shared_t (viewt@ype, int)
fun conats_sharedn_create {a: viewt@ype} {n:pos} (ele: a, n: int n): shared_t (a, n)
fun conats_sharedn_signal {a: viewt@ype} {i,n:nat | i < n} (s: shared_t (a, n), i: int i, ele: a): a
fun conats_sharedn_condwait {a: viewt@ype} {i,n:nat | i < n} (s: shared_t (a, n), i: int i, ele: a): a
|
With such shared object, we can now set up two condition variables handling both full
and empty buffers separately. The complete code can be download here
16_2_producer_consumer_m_1_2cond.dats
. A snappet of code for the producer
is shown below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 | // Keep adding elements into buffer.
fun producer (x: int):<fun1> void = let
val db = conats_shared_acquire (s)
fun insert (db: demo_buffer):<cloref1> demo_buffer = let
val (db, isful) = demo_buffer_isful (db)
in
if isful then let
val db = conats_sharedn_condwait (s, NOTEMP, db)
in
insert (db)
end else let
val (db, isnil) = demo_buffer_isnil (db)
val db = demo_buffer_insert (db)
in
if isnil then conats_sharedn_signal (s, NOTFUL, db)
else db
end
end
val db = insert (db)
val () = conats_shared_release (s, db);
in
producer (x)
end
|
In this implemenation, producer only signals the condition variable when the buffer
is actually empty at that moment. This would lead to the missing of signal if we have
multiple producers and consumers. (Please refer to section 8.2.2 of [2].) In the example
16_3_producer_consumer_m_m_signal.dats
, there is two producers, each of
which inserts only one element, and two consumers, each of which takes out one
element. And the problem of miss signal would lead to deadlock. The model checker
would demonstrate this by a counterexample. One remedy is to sigal the condition
variable every time. The other is to use conats_sharedn_wait instead of
conats_sharedn_signal.