Dining Philosopher with Animation (by Cairo)¶

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11

Copy from
Assignment 3:
Class: BU CAS CS520, Fall, 2013
Due: Thursday, the 26th of September, 2013
*)

(* ****** ****** *)
//
#include
"share/atspre_define.hats"
#include

  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
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205

(*
**
**
**
*)

(* ****** ****** *)

(*
Copy from
Assignment 3:
Class: BU CAS CS520, Fall, 2013
Due: Thursday, the 26th of September, 2013
*)

(* ****** ****** *)
//
#include
"share/atspre_define.hats"
#include
"share/atspre_staload.hats"
//
(* ****** ****** *)

staload
UN = "prelude/SATS/unsafe.sats"

(* ****** ****** *)

staload "libc/SATS/time.sats"

(* ****** ****** *)

staload "{$CAIRO}/SATS/cairo.sats"

(* ****** ****** *)


staload "{$GTK}/SATS/gdk.sats"
staload "{$GTK}/SATS/gtk.sats"
staload "{$GLIB}/SATS/glib.sats"
staload "{$GLIB}/SATS/glib-object.sats"

(* ****** ****** *)

staload "mythread.sats"

// staload "libc/SATS/stdlib.sats"
staload "libc/SATS/unistd.sats"


staload "dp_observer.sats"
dynload "dp_observer.dats"

staload "DiningPhil.sats"
dynload "DiningPhil.dats"
(* ****** ****** *)

%{^
typedef
struct { char buf[32] ; } bytes32 ;
%} // end of [%{^]
abst@ype bytes32 = $extype"bytes32"

(* ****** ****** *)

%{^
#define mystrftime(bufp, m, fmt, ptm) strftime((char*)bufp, m, fmt, ptm)
%} // end of [%{^]

(* ****** ****** *)

extern fun worker (darea: !GtkDrawingArea1): void

(* ****** ****** *)
val x: ref int = ref<int>(0)
val cg: ref double = ref<double>(0.0)
val cb: ref double = ref<double>(1.0)


(* ****** ****** *)

%{^
typedef char **charptrptr ;
%} ;
abstype charptrptr = $extype"charptrptr"


(* ****** ****** *)
(* ****** ****** *)
extern
fun{} fexpose (!GtkDrawingArea1): gboolean

implement{
} fexpose (darea) = let
  val () = draw_drawingarea (darea) in GFALSE
end // end of [fexpose]

extern fun{
} dp_anime_main (): void

(* ****** ****** *)

#define nullp the_null_ptr

#define W 400
#define H 400

implement{}
dp_anime_main
  ((*void*)) = () where
{
//
val win0 =
  gtk_window_new (GTK_WINDOW_TOPLEVEL)
val win0 = win0
val () = assertloc (ptrcast(win0) > 0)
val () = gtk_window_set_default_size (win0, (gint)W, (gint)H)
//
val opt = stropt_some"dining philosopher"
val issome = stropt_is_some(opt)
//
val () =
if issome then let
  val title = stropt_unsome (opt)
in
  gtk_window_set_title (win0, gstring(title))
end // end of [if] // end of [val]
//
val darea =
  gtk_drawing_area_new ()
val p_darea = gobjref2ptr (darea)
val () = assertloc (p_darea > 0)
val () = gtk_container_add (win0, darea)
//
val _sid = g_signal_connect
(
  darea, (gsignal)"expose-event", G_CALLBACK(fexpose), (gpointer)nullp
)
//
val _sid = g_signal_connect
(
  win0, (gsignal)"delete-event", G_CALLBACK(gtk_main_quit), (gpointer)nullp
)
val _sid = g_signal_connect
(
  win0, (gsignal)"destroy-event", G_CALLBACK(gtk_widget_destroy), (gpointer)nullp
)
//
val () = gtk_widget_show_all (win0)
//
val () = g_object_unref (win0) // HX: refcount of [win0] decreases from 2 to 1
//
// todo: Why does this pass the typechecking?
val () = mythread_create_cloptr (llam () => worker (darea))
val () = dp_init ()

//
val ((*void*)) = gtk_main ((*void*))

val () = g_object_unref (darea)
//
} // end of [dp_anime_main]

(* ****** ****** *)

implement
main0 (argc, argv) =
{
//
var argc: int = argc
var argv: charptrptr = $UN.castvwtp1{charptrptr}(argv)
//
val () = $extfcall (void, "gtk_init", addr@(argc), addr@(argv))

val ((*void*)) = dp_anime_main ((*void*))
//
} (* end of [main0] *)

implement worker (darea) = let
  val () = ignoret (sleep(1))
  //
  val (fpf_win | win) = gtk_widget_get_window (darea)
  //
  val isnot = g_object_isnot_null (win) 
  //
  prval () = minus_addback (fpf_win, win | darea)
  //
  in
  //
  if isnot then let
    var alloc: GtkAllocation
    val () = gtk_widget_get_allocation (darea, alloc)
    val () = gtk_widget_queue_draw_area (darea, (gint)0, (gint)0, alloc.width, alloc.height)
  in
    worker(darea)
  end else
    ()
  // end of [if]
  //
end // end of [worker]

(* ****** ****** *)

(* end of [dp_gui.dats] *)

Operations pertaining to array0¶

Ghosts for Model Checking¶

ATS programming language allows programmers to write code constructing proofs along side with operational code which does the actual computation. The code for proof is seen only by the type checker of ATS and is erased completely before the compiler of ATS starts generating executable programs. We extends such concept by allowing programmers to write code related to model checking. Such code can be seen by the type checker of ATS, which facilitate the type checking process, and will be erased (just like proof code) before the compiler of ATS starts generating executable programs. We call such code ghost code. Ghost code comes in various forms: Ghost function, Ghost value, Ghost type, and etc. We will talk about them in details when meeting related exampels.

Both operational code and ghost code have semantics to model checker we build. On the other hand, proof code is neglected by the model checker. The simplest but maybe the most stimulating example of ghost code is mc_assert as shown below.

1
2
3
4
5
6

  fun foo (): void = let
    prval () = mc_assert (false)
  in
  end

  val () = foo ()

The executable generated by ATS compiler from the code above simply does nothing since the only content of the function foo is a ghost function mc_assert, which is only meaningful to our model checker. Intuitively, we can view mc_assert as assertions normally used by programmers for runtime checking, but this time it’s used at the stage of model checking.

Feel free to try the example using our online model checker. To use the model checker, we need to appending the following code to indicate that we want to verify that mc_assert succeeds.

1
2
3

  %{$
  #assert main |= G sys_assertion;
  %}

The complete code (with some routine code for header files) for the example can be found here demo_01_mc_assert.dats

With mc_assert, we can use model checking as a test facility as shown in the following example.

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12

  typedef Int = [x:int] int x

  fun sum {x:nat} (x: int x): Int = x * (x + 1) / 2

  fun sum2 {x:nat}.<x>.(x: int x):<fun> Int =
    if x > 0 then x + sum2 (x - 1)
    else 0

  val n = 3
  val ret = sum (n)
  prval mc_ret = sum2 (n)
  prval () = mc_assert (ret = mc_ret)

In the example above, we have two versions of the summation function. We use model checking to verify that they generate the same output. mc_ret is a ghost value (declared via the keyword prval), and accordingly the executable generated by ATS compiler doesn’t contain the invocation of sum2. However sum2 itself is not a ghost function, and it can be used at runtime if programmers choose to. (Just for technical detail, currently only pure functions in ATS can be used to calculate ghost values. That’s why the type of sum2 is a little bit verbose, since we prove that sum2 always terminates.)

One thing worth mentioning is the type of mc_assert as shown below:

prfun mc_assert {b: bool} (x: bool b):<fun> [b == true] void

The type of the argument of mc_assert depends on a boolean value b in the statics of ATS. mc_assert assures the type system that b is true and as such the type checking of the whole program may be established successfully. Also the validity of such assertion is checking during the process of model checking.

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.

 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

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

 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

Accessing Global Ghost Variables¶

 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
26
27
28
29

  stacst sid_init: sid
  extern val mc_init: mc_gv_t sid_init

  fun exec (x: int): void = let

    fun foo {init: pos}(pf: int_value_of (sid_init, init) | x: int): int = x

    prval (pf | init) = mc_get_int (mc_init)

    // mc_assert cannot be omitted though it is ghost code.
    prval () = mc_assert (init > 0)

    val _ = foo (pf | x)
  in
  end

  val tid1 = conats_tid_allocate ()

  val () = conats_thread_create(exec, 0, tid1)

  prval () = mc_set_int (mc_init, 1)


  %{$
  // #assert main deadlockfree;

  #assert main |= G sys_assertion;

  %}

stacst sid_init: sid
extern val mc_init: mc_gv_t sid_init

fun foo {init: pos}(pf: int_value_of (sid_init, init) | x: int): int = x

fun exec (x: int): void = let

  fun foo {init: pos}(pf: int_value_of (sid_init, init) | x: int): int = x

  prval (pf | init) = mc_get_int (mc_init)

  // mc_assert cannot be omitted though it is ghost code.
  prval () = mc_assert (init > 0)

  val _ = foo (pf | x)
in
end

val tid1 = conats_tid_allocate ()

val () = conats_thread_create(exec, 0, tid1)

prval () = mc_set_int (mc_init, 1)

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23

  stacst mid: sid

  extern val mc_m: mc_gv_t mid

  fun foo1 (): void = let
    prval () = mc_atomic_start()
    prval () = mc_set_int (mc_m, 3)
    prval () = mc_set_int (mc_m, 4)
    prval () = mc_atomic_end()
  in
  end

  fun foo2 (x: int): void = let
    prval (pf | x) = mc_get_int (mc_m)
    prval () = mc_assert (x <> 3)
  in
  end

  val tid1 = conats_tid_allocate ()

  val () = conats_thread_create(foo2, 0, tid1)

  val () = foo1 ()

Virtual Lock¶

Improper handling of resources (e.g. memory) in a program may lead to various bugs (e.g. memroy leak) in sequential programs. The problem gets even worse when entering the concurrent domain, in which simultaneous access to shared resource by multiple threads is feasible. One example is that we may lose the integrity of data if two threads are using a shared memory to transfer data. Techniques for solving this problem generally rely on mutual exclusion principles to control access to shared resources. Mutual exclusion introduces a measure of synchronization, but with the cost of losing efficiency. With a deliberate design, sometimes we can remove the need for synchronization while maintaining the desired property of mutual exclusion. Simpson’s four-slot fully asynchronous communication mechanism [1] demonstrates such idea. However, it’s very difficult to verify that the deemed mutual exclusion property actually holds in the design. To tackle this problem, we provide two primitives supporting the concept of “virtual lock” to allow programmers to specify assumptions of mutual exclusion to various granularities according to their design. And such assumption can then be verified by our model checker.

Let’s illustrate the usage of “virtual lock” using the following example of two-slot mechanism. Consider the scenario in which one writer and one reader try to communicate via a shared resource consisting of multiple memory regions (two in this example). Due to hardware constraint, access to each memory region cannot be done atomically. Therefore, reader may get inconsistent data if writer is writing the same region at the same time. The following code shows the proposed types for the shared resource (dataslots_t) as well as the interfaces for accessing it.

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16

  abstype dataslots_t (t@ype, int)

  absviewtype own_slot_vt (int)

  fun dataslots_create {a:t@ype} {x:pos} (
    x: int x, v: a): dataslots_t (a, x)

  fun dataslots_update {a:t@ype} {x,i:nat | i < x}
    ( vpf: own_slot_vt (i)
    | slots: dataslots_t (a, x), i: int i, v: a
    ): (own_slot_vt i | void)

  fun dataslots_get {a:t@ype} {x,i:nat | i < x}
    ( vpf: own_slot_vt (i)
    | slots: dataslots_t (a, x), i: int i
    ): (own_slot_vt i | a)

The usage of linear type own_slot_vt states clearly that dataslots_update and dataslots_get require mutual exclusion on the memory region to be accessed. Normally, programmers ensure such property by the usage of synchronization primitives (e.g. mutex). However, in the following code, we try to gain mutual exclusion by the usage of a few global variables the access for which is atomic. The code 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
26
27
28

  typedef data_t = dataslots_t (int, 2)
  val data: data_t = dataslots_create (2, 0)

  typedef int2 = [i: int | i >= 0 && i <= 1] int i

  // control variables
  val latest = conats_atomref_create {int2} (0)

  fun write (item: int): void = let
    val index = 1 - conats_atomref_get (latest)

    prval vpf = mc_acquire_ownership (index)
    val (vpf | _) = dataslots_update (vpf | data, index, item)
    prval () = mc_release_ownership (vpf)

    val () = conats_atomref_update (latest, index)
  in
  end

  fun read (): int = let
    val index = conats_atomref_get (latest)

    prval vpf = mc_acquire_ownership (index)
    val (vpf | item) = dataslots_get (vpf | data, index)
    prval () = mc_release_ownership (vpf)
  in
    item
  end

In the example, the shared resource (data_t) contains two regions (slots). lastest is a global reference for an integer, which is created by the primitive conats_atomref_create. (Primitives conats_atomref_create, conats_atomref_get, and conats_atomref_update are provided as an extension to ATS to support concurrent programming.) To pass the type checking of ATS, we use two functions mc_acquire_ownership and mc_release_ownership to generate and destroy the linear ghost value (vpf), which serves as the warranty for mutual exclusion. mc_acquire_ownership and mc_release_ownership are not primitives. Instead, they are user-defined ghost functions. Their implementation is shown below.

1
2
3
4
5

    prfun mc_acquire_ownership .<>. {i: nat}
      (i: int i): own_slot_vt (i) = mc_vlock_get (i, 0, 1, 1)

    prfun mc_release_ownership .<>. {i: nat}
      (vpf: own_slot_vt (i)): void = mc_vlock_put (vpf)

The two ghost functions are built upon two primitives mc_vlock_put and mc_vlock_get. Intuitively, mc_vlock_get (x, y, a, b) indicates the acquision of a virtual lock covering a rectangle with (x, y) as the upper left corner, a as the width (x-axis), and b as the height (y-axis), and mc_vlock_put indicates the release of the lock. And our model checker would check that under no circumstances would two threads try to acquire two virtual locks covering overlapping areas simutaneously. And this serves as the verification of mutual exclusion. To model checking the example, we would need to add the following code to implement those interfaces for accessing shared resource.

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21

  fun dataslots_create {a:t@ype} {x:pos} (
    x: int x, v: a): dataslots_t (a, x) =
     conats_atomarrayref_create {a} (x, v)

  fun dataslots_update {a:t@ype} {x,i:nat | i < x}
    ( vpf: own_slot_vt (i)
    | slots: dataslots_t (a, x), i: int i, v: a
    ): (own_slot_vt i | void) = let
    val () = conats_atomarrayref_update (slots, i, v)
  in
    (vpf | ())
  end

  fun dataslots_get {a:t@ype} {x,i:nat | i < x}
    ( vpf: own_slot_vt (i)
    | slots: dataslots_t (a, x), i: int i
    ): (own_slot_vt i | a) = let
    val v = conats_atomarrayref_get (slots, i)
  in
    (vpf | v)
  end

In the aforementioned code, this implementation is actually based on the primitives for creating and accessing array. This is not necessary if our focus is to verify the validity of mutual exclusion.

The complete code can be downloaded here 20_1_two_slot_acm.dats. Without much thinking, we know that this implementation cannot pass model checking since writer just switches between two slots. Going further, the implementation (20_2_three_slot_acm.dats) using three slots doesn’t work either. And based on the implementation using four slots (20_3_four_slot_acm.dats), we verify that Simpson’s four-slot asynchronous mechanism possesses the acclaimed mutual exclusion property.