Effective ATS:
Readers-and-Writers

In general, ATS shines much more brightly in contexts where dynamic testing becomes more difficult to perform and/or control. In this article, I present in ATS an implementation of the classic Readers-and-Writers problem in concurrent programming.

Description of the Problem

The Readers-and-Writers problem models access to a database. In order for a process to read from the database, the process must be granted a read-access. In order for it to write to the database, it must be granted a write-access. It is not allowed for a read-access and a write-access to be granted at the same time. While multiple read-accesses can be granted simultaneously, only one write-access can be granted at a time.

Interface for Database Access

Following is an abstract interface for accessing database:

//
abstype DB = ptr
//
absview DBread_v
absview DBwrite_v
//
fun DBread (pf: !DBread_v | db: DB): void
fun DBwrite (pf: !DBwrite_v | db: DB): void
//

For calling DBread to read from a database, a proof of the (abstract) view DBread_v is needed. For calling DBwrite to write into a database, a proof of the (abstract) view DBwrite_v is needed.

Databases-with-state

Let us introduce a linear abstract type DBshell for a database with some linear state:

//
absvtype
DBshell (r: int, w: int) = ptr
//
vtypedef DBshell = [r,w:int] DBshell (r, w)
//

Given integer r and w, a value of the type DBshell(r, w) is referred to as a database-with-state in which the associated database is currently granting r read-accesses and w write-accesses. The following two proof functions mention explicitly some constraints on parameters r and w:

//
praxi
lemma_DBshell_param
  {r,w:int} (!DBshell (r, w)): [0 <= r; 0 <= w; w <= 1] void
praxi
lemma_DBshell_param2
  {r,w:int} (!DBshell (r, w)): [r == 0 || (r > 0 && w == 0)] void
//

Given a type DBshell(r, w), the proof function lemma_DBshell_param states that r is a natural number and w is between 0 and 1, inclusive; the proof function lemma_DBshell_param2 states that w must equal 0 if r is positive.

Some functions on databases-with-state are listed as follows:

//
fun DBshell_dbget (x: !DBshell): DB
//
fun DBshell_nread {r,w:int} (x: !DBshell (r, w)): int (r)
fun DBshell_nwrite {r,w:int} (x: !DBshell (r, w)): int (w)
//

Clearly, DBshell_dbget is meant to return the database associated with a given database-with-state. As for DBshell_nread and DBshell_nwrite, they can be called on a database-with-state of type DBshell(r, w) to obtain the values of r and w, respectively.

Encoding the Policy for Database Access

The policy for database access is formally encoded in the types of the following declared functions:

//
fun DBshell_acquire_read
  {r:int} (x: !DBshell (r, 0) >> DBshell (r+1, 0)): (DBread_v | void)
fun DBshell_release_read
  {r,w:int} (pf: DBread_v | x: !DBshell (r, w) >> DBshell (r-1, w)): void
//
fun DBshell_acquire_write
  (x: !DBshell (0, 0) >> DBshell (0, 1)): (DBwrite_v | void)
fun DBshell_release_write
  {r,w:int} (pf: DBwrite_v | x: !DBshell (r, w) >> DBshell (r, w-1)): void
//

A proof of the view DBread_v is needed for reading from a database. In order to obtain it, DBshell_acquire_read needs to be called on a database-with-state that is currently granting no write-access. Similarly, a proof of the view DBwrite_v is needed for writing to a database. In order to obtain it, DBshell_acquire_write needs to be called on a database-with-state that is currently granting neither read-access nor write-access.

Shared Databases-with-state

A shared database-with-state essentially wraps a protection mechanism around a database-with-state. Let introduce a non-linear abstract type SDBshell for shared databases-with-state:

abstype SDBshell = ptr

As can be expected, there is a mutex for protecting the database-with-state inside a shared database-with-state. The following two functions can be called to acquire/release the protected database-with-state:

fun SDBshell_acquire (sx: SDBshell): DBshell
fun SDBshell_release (sx: SDBshell, x: DBshell): void

Let us now see an implementation of the following declared functions:

//
fun SDBshell_acquire_read (sx: SDBshell): (DBread_v | void)
fun SDBshell_release_read (pf: DBread_v | sx: SDBshell): void
//
fun SDBshell_acquire_write (sx: SDBshell): (DBwrite_v | void) 
fun SDBshell_release_write (pf: DBwrite_v | sx: SDBshell): void
//

which can be called to safely support database access in concurrent programming (without causing race conditions).

There is a conditional variable (CV) inside a shared database-with-state. The following function SDBshell_wait_read can be called by a process to wait on the CV if it wants to read but the database is currently granting a write-access to another process:

//
extern
fun SDBshell_wait_read
  {r:int}
(
  sx: SDBshell, x: !DBshell (r, 1) >> DBshell
) : void // end of [SDBshell_wait_read]
//

Similarly, the following function SDBshell_wait_write can be called by a process to wait on the CV if it wants to write but the database is currently granting a read-access or write-access to another process:

extern
fun SDBshell_wait_write
  {r,w:int | r+w >= 1}
(
  sx: SDBshell, x: !DBshell (r, w) >> DBshell
) : void // end of [SDBshell_wait_write]

In order to wake up a process waiting on the conditional variable, the following function SDBshell_signal can be called:

//
extern fun SDBshell_signal (sx: SDBshell): void
//

Furthermore, two auxiliary functions are declared as follows to facilitate the implementation of SDBshell_acquire_read and SDBshell_acquire_write:

extern
fun SDBshell_acquire_read2
  (sx: SDBshell, x: !DBshell >> _): (DBread_v | void)
extern
fun SDBshell_acquire_write2
  (sx: SDBshell, x: !DBshell >> _): (DBwrite_v | void)

The following code implements SDBshell_acquire_read:

implement
SDBshell_acquire_read
  (sx) = (pf | ()) where
{
  val x = SDBshell_acquire (sx)
  val (pf | ()) = SDBshell_acquire_read2 (sx, x)
  val () = SDBshell_release (sx, x)
}

implement
SDBshell_acquire_read2
  (sx, x) = let
//
prval () =
  lemma_DBshell_param (x)
//
val w = DBshell_nwrite (x)
//
in
//
if w = 0
  then DBshell_acquire_read (x)
  else let
    val () = SDBshell_wait_read (sx, x) in SDBshell_acquire_read2 (sx, x)
  end // end of [else]
//
end // end of [SDBshell_acquire_read2]

The following code implements SDBshell_release_read:

implement
SDBshell_release_read
  (pf | sx) = () where
{
  val x = SDBshell_acquire (sx)
  val () = DBshell_release_read (pf | x)
  val r = DBshell_nread (x)
  val () =
    if r = 0
      then SDBshell_signal (sx)
    // end of [if]
  val () = SDBshell_release (sx, x)
}

The following code implements SDBshell_acquire_write:

implement
SDBshell_acquire_write
  (sx) = (pf | ()) where
{
  val x = SDBshell_acquire (sx)
  val (pf | ()) = SDBshell_acquire_write2 (sx, x)
  val () = SDBshell_release (sx, x)
}

implement
SDBshell_acquire_write2
  (sx, x) = let
//
prval () =
  lemma_DBshell_param (x)
prval () =
  lemma_DBshell_param2 (x)
//
val r = DBshell_nread (x)
//
in
//
if r = 0
  then let
    val w = DBshell_nwrite (x)
  in
    if w = 0
      then DBshell_acquire_write (x)
      else let
        val () = SDBshell_wait_write (sx, x)
      in
        SDBshell_acquire_write2 (sx, x)
      end // end of [else]
    // end of [if]
  end // end of [then]
  else let
    val () = SDBshell_wait_write (sx, x) in SDBshell_acquire_write2 (sx, x)
  end // end of [else]
//
end // end of [SDBshell_acquire_write2]

The following code implements SDBshell_release_write:

implement
SDBshell_release_write
  (pf | sx) = () where
{
  val x = SDBshell_acquire (sx)
  val () = DBshell_release_write (pf | x)
  val () = SDBshell_signal (sx)
  val () = SDBshell_release (sx, x)
}

Summary of the Remaining Implementation

Please find the entirety of the code in the following files:

DB_read_write.sats
DB_read_write.dats

This article is written by Hongwei Xi.