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