@@ -75,6 +75,7 @@ is distributed under the [ISC license](LICENSE.md).
7575 - [ Programming with transactional data structures] ( #programming-with-transactional-data-structures )
7676 - [ The dining philosophers problem] ( #the-dining-philosophers-problem )
7777 - [ A transactional LRU cache] ( #a-transactional-lru-cache )
78+ - [ The sleeping barbers problem] ( #the-sleeping-barbers-problem )
7879- [ Designing lock-free algorithms with k-CAS] ( #designing-lock-free-algorithms-with-k-cas )
7980 - [ Understand performance] ( #understand-performance )
8081 - [ Minimize accesses] ( #minimize-accesses )
@@ -1036,6 +1037,270 @@ val a_cache : (int, string) cache =
10361037As an exercise, implement an operation to ` remove ` associations from a cache and
10371038an operation to change the capacity of the cache.
10381039
1040+ #### The sleeping barbers problem
1041+
1042+ The
1043+ [ sleeping barber problem] ( https://en.wikipedia.org/wiki/Sleeping_barber_problem )
1044+ is another classic communication and synchronization problem. Let's write a
1045+ solution using ** Kcas** .
1046+
1047+ There are
1048+ [ many ways to solve the problem] ( https://en.wikipedia.org/wiki/Sleeping_barber_problem#Solutions )
1049+ and, in particular, there are concise and subtle implementations using
1050+ semaphores or mutexes. Instead of transliterating a solution using semaphores,
1051+ our approach uses queues and other concurrent data structures. We also solve the
1052+ generalized problem with multiple barbers and we also implement a mechanism to
1053+ close the barbershop. In addition, we abstract the concept of a barbershop,
1054+ where barbers and customers interact. All of this makes our solution longer than
1055+ the well known semaphore based solution. On the other hand, one might argue that
1056+ our solution is a more direct transliteration of the problem. Our solution also
1057+ avoids the starvation problem by using queues.
1058+
1059+ Let's begin by abstracting customer
1060+
1061+ ``` ocaml
1062+ type customer = {
1063+ notify_hair_has_been_cut : 'x.xt:'x Xt.t -> unit;
1064+ }
1065+ ```
1066+
1067+ and barber
1068+
1069+ ``` ocaml
1070+ type barber = {
1071+ wake_up : 'x.xt:'x Xt.t -> customer -> unit;
1072+ }
1073+ ```
1074+
1075+ actors. The idea is that barbers notify customers after finishing their haircut
1076+ and, adhering to the problem description, customers wake up sleeping barbers.
1077+
1078+ A barbershop consists of any number of barbers and waiting customers and can be
1079+ marked as closed:
1080+
1081+ ``` ocaml
1082+ type barbershop = {
1083+ sleeping_barbers : barber Queue.t;
1084+ waiting_customers : customer Queue.t;
1085+ is_closed : bool Loc.t;
1086+ }
1087+ ```
1088+
1089+ The barbershop constructor does not limit the number of barbers, which are
1090+ assumed to bring their own chairs, but does require a specification of the
1091+ number of waiting room chairs for customers:
1092+
1093+ ``` ocaml
1094+ # let barbershop ~num_waiting_chairs =
1095+ let sleeping_barbers = Queue.create ()
1096+ and waiting_customers = Queue.create ~capacity:num_waiting_chairs ()
1097+ and is_closed = Loc.make false in
1098+ { sleeping_barbers; waiting_customers; is_closed }
1099+ val barbershop : num_waiting_chairs:int -> barbershop = <fun>
1100+ ```
1101+
1102+ Although the ` barbershop ` type is not abstract, we treat it as such, so we
1103+ provide a transactional predicate to check whether the barbershop is closed or
1104+ not:
1105+
1106+ ``` ocaml
1107+ # let is_closed ~xt bs = Xt.get ~xt bs.is_closed
1108+ val is_closed : xt:'a Xt.t -> barbershop -> bool = <fun>
1109+ ```
1110+
1111+ To ` close ` a barbershop we set the ` is_closed ` location to ` true ` and clear both
1112+ the sleeping barbers and waiting customers queues:
1113+
1114+ ``` ocaml
1115+ # let close ~xt bs =
1116+ Xt.set ~xt bs.is_closed true;
1117+ Queue.Xt.clear ~xt bs.sleeping_barbers;
1118+ Queue.Xt.clear ~xt bs.waiting_customers
1119+ val close : xt:'a Xt.t -> barbershop -> unit = <fun>
1120+ ```
1121+
1122+ A barber can try to get a customer sitting on a waiting room chair:
1123+
1124+ ``` ocaml
1125+ # let get_sitting_customer_opt ~xt bs =
1126+ Queue.Xt.take_opt ~xt bs.waiting_customers
1127+ val get_sitting_customer_opt : xt:'a Xt.t -> barbershop -> customer option =
1128+ <fun>
1129+ ```
1130+
1131+ Or may go to sleep on the barber's own chair:
1132+
1133+ ``` ocaml
1134+ # let sleep ~xt bs barber =
1135+ if not (is_closed ~xt bs) then
1136+ Queue.Xt.add ~xt barber bs.sleeping_barbers
1137+ val sleep : xt:'a Xt.t -> barbershop -> barber -> unit = <fun>
1138+ ```
1139+
1140+ Note that the ` sleep ` transaction uses the ` is_closed ` predicate. Barbers, as
1141+ well as customers, must leave the shop in case it is closed.
1142+
1143+ A customer can try to find a sleeping barber:
1144+
1145+ ``` ocaml
1146+ # let get_sleeping_barber_opt ~xt bs =
1147+ Queue.Xt.take_opt ~xt bs.sleeping_barbers
1148+ val get_sleeping_barber_opt : xt:'a Xt.t -> barbershop -> barber option =
1149+ <fun>
1150+ ```
1151+
1152+ Or sit on a waiting room chair:
1153+
1154+ ``` ocaml
1155+ # let try_sitting ~xt bs customer =
1156+ not (is_closed ~xt bs) &&
1157+ Queue.Xt.try_add ~xt customer bs.waiting_customers
1158+ val try_sitting : xt:'a Xt.t -> barbershop -> customer -> bool = <fun>
1159+ ```
1160+
1161+ The above ` try_sitting ` transaction is non-blocking. In case the
1162+ ` waiting_customers ` queue is full, it will return ` false ` . With the ` customer `
1163+ actor implementation we'll look at shortly this would mean that customers would
1164+ busy-wait, which works, but potentially wastes energy. Here is a blocking
1165+ version of ` try_sitting ` :
1166+
1167+ ``` ocaml
1168+ # let try_sitting ~xt bs customer =
1169+ not (is_closed ~xt bs) &&
1170+ begin
1171+ Queue.Xt.add ~xt customer bs.waiting_customers;
1172+ true
1173+ end
1174+ val try_sitting : xt:'a Xt.t -> barbershop -> customer -> bool = <fun>
1175+ ```
1176+
1177+ Both of the above ` try_sitting ` transactions work with the ` customer ` actor
1178+ we'll see shortly, but with the latter blocking version we avoid busy-wait.
1179+
1180+ The above constitutes the barbershop abstraction which is a kind of passive
1181+ concurrent data structure. Let's then implement the active participants of the
1182+ problem.
1183+
1184+ A customer tries to get a haircut. When a customer enter the barbershop he first
1185+ tries to find a sleeping barber. If none is available, the customer then tries
1186+ to sit on a waiting room chair. If both fail, then the customer has no option
1187+ except to retry. Otherwise the customer waits to get a haircut. If the shop is
1188+ closed, the customer exits. Here is the ` customer ` actor:
1189+
1190+ ``` ocaml
1191+ # let customer shop cuts =
1192+ let clean = Mvar.create None in
1193+ let self = { notify_hair_has_been_cut = Mvar.Xt.put clean true } in
1194+ while not (Xt.commit { tx = is_closed shop }) do
1195+ let get_barber_opt ~xt =
1196+ match get_sleeping_barber_opt ~xt shop with
1197+ | None ->
1198+ try_sitting ~xt shop self
1199+ | Some barber ->
1200+ barber.wake_up ~xt self;
1201+ true
1202+ in
1203+ if Xt.commit { tx = get_barber_opt } then
1204+ let try_await_haircut ~xt =
1205+ not (is_closed ~xt shop) &&
1206+ Mvar.Xt.take ~xt clean
1207+ in
1208+ if Xt.commit { tx = try_await_haircut } then
1209+ Loc.incr cuts
1210+ done
1211+ val customer : barbershop -> int Loc.t -> unit = <fun>
1212+ ```
1213+
1214+ A barber tries to get a customer to give a haircut. A barber first looks for a
1215+ customer from the waiting room. If none is available, the barber goes to sleep
1216+ waiting for a wakeup from a customer. After obtaining a customer in either way,
1217+ the barber gives a haircut to the customer. Otherwise the shop must be closed
1218+ and the barber exits. Here is the ` barber ` actor:
1219+
1220+ ``` ocaml
1221+ # let barber shop cuts =
1222+ let customer = Mvar.create None in
1223+ let self = { wake_up = Mvar.Xt.put customer } in
1224+ while not (Xt.commit { tx = is_closed shop }) do
1225+ let cut customer =
1226+ Xt.commit { tx = customer.notify_hair_has_been_cut };
1227+ Loc.incr cuts
1228+ in
1229+ let get_customer_opt ~xt =
1230+ match get_sitting_customer_opt ~xt shop with
1231+ | Some _ as some -> some
1232+ | None ->
1233+ sleep ~xt shop self;
1234+ None
1235+ in
1236+ match Xt.commit { tx = get_customer_opt } with
1237+ | Some customer -> cut customer
1238+ | None ->
1239+ let await_wakeup_opt ~xt =
1240+ if is_closed ~xt shop then None
1241+ else Some (Mvar.Xt.take ~xt customer)
1242+ in
1243+ match Xt.commit { tx = await_wakeup_opt } with
1244+ | Some customer -> cut customer
1245+ | None -> ()
1246+ done
1247+ val barber : barbershop -> int Loc.t -> unit = <fun>
1248+ ```
1249+
1250+ To run the problem, a barbershop is created with given number of waiting room
1251+ chairs, is populated by given number of barbers, and a given number of customers
1252+ are spawned. Once each barber has given and each customer has received a given
1253+ number of haircuts the shop is closed. This termination condition seeks to
1254+ demonstrate that no actor is starved. Here is the ` sleeping_barbers ` setup:
1255+
1256+ ``` ocaml
1257+ # let sleeping_barbers ~barbers
1258+ ~num_waiting_chairs
1259+ ~customers
1260+ ~cuts_per_actor =
1261+ assert (0 < barbers
1262+ && 0 <= num_waiting_chairs
1263+ && 0 <= customers
1264+ && 0 <= cuts_per_actor);
1265+ let shop = barbershop ~num_waiting_chairs in
1266+ let barbers = Array.init barbers @@ fun _ ->
1267+ let cuts = Loc.make 0 in
1268+ (cuts, Domain.spawn @@ (fun () -> barber shop cuts))
1269+ and customers = Array.init customers @@ fun _ ->
1270+ let cuts = Loc.make 0 in
1271+ (cuts, Domain.spawn @@ (fun () -> customer shop cuts))
1272+ in
1273+ let agents = Array.append barbers customers in
1274+ while agents
1275+ |> Array.map fst
1276+ |> Array.exists @@ fun c ->
1277+ Loc.get c < cuts_per_actor do
1278+ Domain.cpu_relax ()
1279+ done;
1280+ Xt.commit { tx = close shop };
1281+ agents
1282+ |> Array.map snd
1283+ |> Array.iter Domain.join
1284+ val sleeping_barbers :
1285+ barbers:int ->
1286+ num_waiting_chairs:int -> customers:int -> cuts_per_actor:int -> unit =
1287+ <fun>
1288+ ```
1289+
1290+ Finally, let's try our solution:
1291+
1292+ ``` ocaml
1293+ # sleeping_barbers ~barbers:2
1294+ ~num_waiting_chairs:1
1295+ ~customers:4
1296+ ~cuts_per_actor:10
1297+ - : unit = ()
1298+ ```
1299+
1300+ Like mentioned in the beginning, this is not the most concise solution of the
1301+ sleeping barbers problem, but hopefully this solution can be understood
1302+ relatively easily with respect to the problem description.
1303+
10391304## Designing lock-free algorithms with k-CAS
10401305
10411306The key benefit of k-CAS, or k-CAS-n-CMP, and transactions in particular, is
0 commit comments