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:
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: 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: 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 //
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_ //
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]
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]
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]
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.