Introduction to Programming in ATS:
Prev	Chapter 16. Abstract Views and Viewtypes	Next

Locking and Unlocking

In concurrent programming, the issue of safely locking and unlocking shared resources is both essential and challenging. I am to demonstrate in this section concretely and convincingly that linear types can be used with great effectiveness to address this issue.

Let us first introduce a linear abstract type shared as follows:

absvtype shared(a:vtype) = ptr

Given a viewtype VT (for some resources), a value of the type shared(VT) is essentially a boxed record containing a resource of the type VT plus a lock (or several) of some kind. The following function shared_make is called to turn a resource into a shared resource:

fun shared_make{a:vtype}(x: a): shared(a)

Notice that the type shared(VT) itself is linear. In terms of implementation, there is usually a reference count inside a linear shared resource that is protected by a spin-lock. The functions shared_ref and shared_unref are for increasing and descreasing the reference count inside a shared resource:

fun shared_ref{a:vtype}(!shared(a)): shared(a)
fun shared_unref{a:vtype}(shared(a)): Option_vt(a)

If the reference count of a shared resource is 1, then calling shared_unref on the shared resource frees the memory used in its representation and then returns the resource stored inside it.

The function shared_lock acquires the resource from a given shared resource and the function shared_unlock does the opposite:

//
absview locked_v
//
fun shared_lock{a:vtype}(!shared(a)): (locked_v | a)
fun shared_unlock{a:vtype}(locked_v | !shared(a), x: a): void
//

Note that the abstract view locked_v is introduced for linear proofs that are meant to remind the programmer that a shared resoure needs to be released after it is acquired.

As can be expected, a shared resource can be implemented as a boxed tuple consisting of a spin-lock, a reference count and a pointer (referring to the stored resource):

//
datavtype
shared_ (a:vtype) =
  SHARED of (spin1_vt(*lock*), int(*count*), ptr)
//
assume shared = shared_
//

Note that the type spin1_vt is for linear spin-locks. The function shared_ref is implemented as follows:

implement
shared_ref
  {a}(sh) = let
//
val+@SHARED
  (spin, count, _) = sh
//
val
spin = // for temp. use
  unsafe_spin_vt2t(spin)
//
val
(pf | ()) = spin_lock(spin)
val c0 = count
val () = count := c0 + 1
val ((*void*)) = spin_unlock(pf | spin)
prval ((*void*)) = fold@sh
//
in
  $UN.castvwtp1{shared(a)}(sh)
end // end of [shared_ref]

Clearly, the implementation makes use of several unsafe casts. An implementation without such casts would be highly involved even if it could be done. The spin-lock must be acquired before the binding between c0 and the integer stored in count is formed for otherwise a race condition can appear. The function shared_unref is implemented as follows:

implement
shared_unref
  {a}(sh) = let
//
val+@SHARED
  (spin, count, _) = sh
//
val
spin = // for temp. use
  unsafe_spin_vt2t(spin)
//
val
(pf | ()) = spin_lock(spin)
val c0 = count
val () = count := c0 - 1
val ((*void*)) = spin_unlock(pf | spin)
prval ((*void*)) = fold@sh
//
in
//
if
c0 <= 1
then let
  val+~SHARED(spin, _, x) = sh
  val ((*freed*)) = spin_vt_destroy(spin)
in
  Some_vt($UN.castvwtp0{a}(x))
end // end of [then]
else let
  prval () = $UN.cast2void(sh) in None_vt()
end // end of [else]
//
end // end of [shared_unref]

In the case where the reference count is 1, then the shared resource is freed, the spin-lock in it is destroyed, and the resource in it is returned.

The functions shared_lock and shared_unlock are implemented as follows:

implement
shared_lock
  {a}(sh) = let
//
val+@SHARED(spin, _, x) = sh
//
val
spin =
  unsafe_spin_vt2t(spin)
//
val
(pf | ()) = spin_lock(spin)
//
val x0 = $UN.castvwtp0{a}(x)
//
prval () = fold@sh
//
in
  ($UN.castview0(pf) | x0)
end // end of [shared_lock]

implement
shared_unlock
  {a}(pf | sh, x0) = let
//
val+@SHARED(spin, _, x) = sh
//
val
spin =
  unsafe_spin_vt2t(spin)
//
val () = x := $UN.castvwtp0{ptr}(x0)
//
val () =
  spin_unlock($UN.castview0(pf) | spin)
//
prval () = fold@sh
//
in
  // nothing
end // end of [shared_unlock]

In the case of shared_lock, please notice that the content stored in the variable x is read out after the spin-lock is acquired. This is crucial for otherwise a race condition can readily appear. In the case of shared_unlock, the content of the variable x is updated before the acquired spin-lock is released.

Please find on-line the file shared_vt.dats containing the entirety of the code presented in this section. In addition, the file also contains an implementation of three threads that move in locked steps: thread 0 moves; thread 1 moves; thread 2 moves; thread 0 moves; thread 1 moves; thread 2 moves; etc.

Prev	Home	Next
Example: Array-Based Circular Buffers	Up	Linear Channels for Asynchronous IPC