Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Provide semaphores in the threading library (#9930)
This commit adds a new thread-related module Semaphore, implementing counting semaphores and binary semaphores. The two kinds of semaphores are presented as two different abstract types in two sub-modules, Counting and Binary.
- Loading branch information
1 parent
f809e9d
commit 426b10c
Showing
8 changed files
with
249 additions
and
4 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,86 @@ | ||
(**************************************************************************) | ||
(* *) | ||
(* OCaml *) | ||
(* *) | ||
(* Xavier Leroy, Collège de France and INRIA Paris *) | ||
(* *) | ||
(* Copyright 2020 Institut National de Recherche en Informatique et *) | ||
(* en Automatique. *) | ||
(* *) | ||
(* All rights reserved. This file is distributed under the terms of *) | ||
(* the GNU Lesser General Public License version 2.1, with the *) | ||
(* special exception on linking described in the file LICENSE. *) | ||
(* *) | ||
(**************************************************************************) | ||
|
||
(** Semaphores *) | ||
|
||
type sem = { | ||
mut: Mutex.t; (* protects [v] *) | ||
mutable v: int; (* the current value *) | ||
nonzero: Condition.t (* signaled when [v > 0] *) | ||
} | ||
|
||
module Counting = struct | ||
|
||
type t = sem | ||
|
||
let make v = | ||
if v < 0 then invalid_arg "Semaphore.Counting.init: wrong initial value"; | ||
{ mut = Mutex.create(); v; nonzero = Condition.create() } | ||
|
||
let release s = | ||
Mutex.lock s.mut; | ||
if s.v < max_int then begin | ||
s.v <- s.v + 1; | ||
Condition.signal s.nonzero; | ||
Mutex.unlock s.mut | ||
end else begin | ||
Mutex.unlock s.mut; | ||
raise (Sys_error "Semaphore.Counting.release: overflow") | ||
end | ||
|
||
let acquire s = | ||
Mutex.lock s.mut; | ||
while s.v = 0 do Condition.wait s.nonzero s.mut done; | ||
s.v <- s.v - 1; | ||
Mutex.unlock s.mut | ||
|
||
let try_acquire s = | ||
Mutex.lock s.mut; | ||
let ret = if s.v = 0 then false else (s.v <- s.v - 1; true) in | ||
Mutex.unlock s.mut; | ||
ret | ||
|
||
let get_value s = s.v | ||
|
||
end | ||
|
||
module Binary = struct | ||
|
||
type t = sem | ||
|
||
let make b = | ||
{ mut = Mutex.create(); | ||
v = if b then 1 else 0; | ||
nonzero = Condition.create() } | ||
|
||
let release s = | ||
Mutex.lock s.mut; | ||
s.v <- 1; | ||
Condition.signal s.nonzero; | ||
Mutex.unlock s.mut | ||
|
||
let acquire s = | ||
Mutex.lock s.mut; | ||
while s.v = 0 do Condition.wait s.nonzero s.mut done; | ||
s.v <- 0; | ||
Mutex.unlock s.mut | ||
|
||
let try_acquire s = | ||
Mutex.lock s.mut; | ||
let ret = if s.v = 0 then false else (s.v <- 0; true) in | ||
Mutex.unlock s.mut; | ||
ret | ||
|
||
end |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,140 @@ | ||
(**************************************************************************) | ||
(* *) | ||
(* OCaml *) | ||
(* *) | ||
(* Xavier Leroy, Collège de France and INRIA Paris *) | ||
(* *) | ||
(* Copyright 2020 Institut National de Recherche en Informatique et *) | ||
(* en Automatique. *) | ||
(* *) | ||
(* All rights reserved. This file is distributed under the terms of *) | ||
(* the GNU Lesser General Public License version 2.1, with the *) | ||
(* special exception on linking described in the file LICENSE. *) | ||
(* *) | ||
(**************************************************************************) | ||
|
||
(** Semaphores | ||
A semaphore is a thread synchronization device that can be used to | ||
control access to a shared resource. | ||
Two flavors of semaphores are provided: counting semaphores and | ||
binary semaphores. | ||
@since 4.12 *) | ||
|
||
(** {2 Counting semaphores} *) | ||
|
||
(** | ||
A counting semaphore is a counter that can be accessed concurrently | ||
by several threads. The typical use is to synchronize producers and | ||
consumers of a resource by counting how many units of the resource | ||
are available. | ||
The two basic operations on semaphores are: | ||
- "release" (also called "V", "post", "up", and "signal"), which | ||
increments the value of the counter. This corresponds to producing | ||
one more unit of the shared resource and making it available to others. | ||
- "acquire" (also called "P", "wait", "down", and "pend"), which | ||
waits until the counter is greater than zero and decrements it. | ||
This corresponds to consuming one unit of the shared resource. | ||
@since 4.12 *) | ||
|
||
module Counting : sig | ||
|
||
type t | ||
(** The type of counting semaphores. *) | ||
|
||
val make : int -> t | ||
(** [make n] returns a new counting semaphore, with initial value [n]. | ||
The initial value [n] must be nonnegative. | ||
@raise Invalid_argument if [n < 0] | ||
*) | ||
|
||
val release : t -> unit | ||
(** [release s] increments the value of semaphore [s]. | ||
If other threads are waiting on [s], one of them is restarted. | ||
If the current value of [s] is equal to [max_int], the value of | ||
the semaphore is unchanged and a [Sys_error] exception is raised | ||
to signal overflow. | ||
@raise Sys_error if the value of the semaphore would overflow [max_int] | ||
*) | ||
|
||
val acquire : t -> unit | ||
(** [acquire s] blocks the calling thread until the value of semaphore [s] | ||
is not zero, then atomically decrements the value of [s] and returns. | ||
*) | ||
|
||
val try_acquire : t -> bool | ||
(** [try_acquire s] immediately returns [false] if the value of semaphore [s] | ||
is zero. Otherwise, the value of [s] is atomically decremented | ||
and [try_acquire s] returns [true]. | ||
*) | ||
|
||
val get_value : t -> int | ||
(** [get_value s] returns the current value of semaphore [s]. | ||
The current value can be modified at any time by concurrent | ||
{!release} and {!acquire} operations. Hence, the [get_value] | ||
operation is racy, and its result should only be used for debugging | ||
or informational messages. | ||
*) | ||
|
||
end | ||
|
||
(** {2 Binary semaphores} *) | ||
|
||
(** Binary semaphores are a variant of counting semaphores | ||
where semaphores can only take two values, 0 and 1. | ||
A binary semaphore can be used to control access to a single | ||
shared resource, with value 1 meaning "resource is available" and | ||
value 0 meaning "resource is unavailable". | ||
The "release" operation of a binary semaphore sets its value to 1, | ||
and "acquire" waits until the value is 1 and sets it to 0. | ||
A binary semaphore can be used instead of a mutex (see module | ||
{!Mutex}) when the mutex discipline (of unlocking the mutex from the | ||
thread that locked it) is too restrictive. The "acquire" operation | ||
corresponds to locking the mutex, and the "release" operation to | ||
unlocking it, but "release" can be performed in a thread different | ||
than the one that performed the "acquire". Likewise, it is safe | ||
to release a binary semaphore that is already available. | ||
@since 4.12 | ||
*) | ||
|
||
module Binary : sig | ||
|
||
type t | ||
(** The type of binary semaphores. *) | ||
|
||
val make : bool -> t | ||
(** [make b] returns a new binary semaphore. | ||
If [b] is [true], the initial value of the semaphore is 1, meaning | ||
"available". If [b] is [false], the initial value of the | ||
semaphore is 0, meaning "unavailable". | ||
*) | ||
|
||
val release : t -> unit | ||
(** [release s] sets the value of semaphore [s] to 1, putting it in the | ||
"available" state. If other threads are waiting on [s], one of them is | ||
restarted. | ||
*) | ||
|
||
val acquire : t -> unit | ||
(** [acquire s] blocks the calling thread until the semaphore [s] | ||
has value 1 (is available), then atomically sets it to 0 | ||
and returns. | ||
*) | ||
|
||
val try_acquire : t -> bool | ||
(** [try_acquire s] immediately returns [false] if the semaphore [s] | ||
has value 0. If [s] has value 1, its value is atomically set to 0 | ||
and [try_acquire s] returns [true]. | ||
*) | ||
|
||
end |