67 lines
2.5 KiB
Diff
67 lines
2.5 KiB
Diff
From 925bf9a6d828d7548751f9a21892cad6209fc950 Mon Sep 17 00:00:00 2001
|
|
From: Gabriel Scherer <gabriel.scherer@gmail.com>
|
|
Date: Fri, 16 Dec 2022 09:41:13 +0100
|
|
Subject: [PATCH 02/17] Merge pull request #11814 from
|
|
gasche/clarify-DLS.new_key-doc
|
|
|
|
clarify the doc of Domain.DLS.new_key
|
|
|
|
(cherry picked from commit be210179503c4a82b72dd4762560e13c408d37b7)
|
|
---
|
|
stdlib/domain.mli | 37 ++++++++++++++++++++++++++++++-------
|
|
1 file changed, 30 insertions(+), 7 deletions(-)
|
|
|
|
diff --git a/stdlib/domain.mli b/stdlib/domain.mli
|
|
index 7763043aa5..2d79b3b0c3 100644
|
|
--- a/stdlib/domain.mli
|
|
+++ b/stdlib/domain.mli
|
|
@@ -96,15 +96,38 @@ module DLS : sig
|
|
|
|
val new_key : ?split_from_parent:('a -> 'a) -> (unit -> 'a) -> 'a key
|
|
(** [new_key f] returns a new key bound to initialiser [f] for accessing
|
|
- domain-local variables.
|
|
+, domain-local variables.
|
|
|
|
- If [split_from_parent] is provided, spawning a domain will derive the
|
|
- child value (for this key) from the parent value.
|
|
+ If [split_from_parent] is not provided, the value for a new
|
|
+ domain will be computed on-demand by the new domain: the first
|
|
+ [get] call will call the initializer [f] and store that value.
|
|
|
|
- Note that the [split_from_parent] call is computed in the parent
|
|
- domain, and is always computed regardless of whether the child domain
|
|
- will use it. If the splitting function is expensive or requires
|
|
- client-side computation, consider using ['a Lazy.t key].
|
|
+ If [split_from_parent] is provided, spawning a domain will
|
|
+ derive the child value (for this key) from the parent
|
|
+ value. This computation happens in the parent domain and it
|
|
+ always happens, regardless of whether the child domain will
|
|
+ use it.
|
|
+ If the splitting function is expensive or requires
|
|
+ child-side computation, consider using ['a Lazy.t key]:
|
|
+
|
|
+ {[
|
|
+ let init () = ...
|
|
+
|
|
+ let split_from_parent parent_value =
|
|
+ ... parent-side computation ...;
|
|
+ lazy (
|
|
+ ... child-side computation ...
|
|
+ )
|
|
+
|
|
+ let key = Domain.DLS.new_key ~split_from_parent init
|
|
+
|
|
+ let get () = Lazy.force (Domain.DLS.get key)
|
|
+ ]}
|
|
+
|
|
+ In this case a part of the computation happens on the child
|
|
+ domain; in particular, it can access [parent_value]
|
|
+ concurrently with the parent domain, which may require
|
|
+ explicit synchronization to avoid data races.
|
|
*)
|
|
|
|
val get : 'a key -> 'a
|
|
--
|
|
2.41.0
|
|
|