Basic Key API #3485

dkalinichenko-js · 2025-01-17T00:07:10Z

Basic Capsule Key API.

Adds 'k Key.t, a ghost type representing the ownership of a capsule 'k. Keys can be converted to passwords or accesses using with_password and access. Exceptions raised from those are unwrapped to the original, destroying the key in process.

Mutexes and rw-locks are now created using keys and leak keys on destruction.

Shared keys are not implemented yet, pending discussion how to deal with exceptions.

lpw25

A few suggestions, but this looks good.

otherlibs/stdlib_alpha/capsule.ml

lpw25 · 2025-01-17T08:32:29Z

otherlibs/stdlib_alpha/capsule.mli

@@ -44,12 +44,12 @@
 module Name : sig

  type 'k t : value mod global portable many uncontended unique
-  (** A ['k Name.t] represents the identity of a capsule. *)
+  (** A ['k Name.t] represents an identity of a capsule.
+      A capsule can have multiple names. *)


I think once something has multiple names it probably isn’t an “identity”. I think, with the design you have here, it would be better to move Name.t to be Password.Name.t and describe it as the identity of a password instead.

That would also make it easy to delay creating the name until it is asked for from the password by having the password be mutable and hold a dummy value when created. That will avoid needless contention on the atomic used for allocating names.

Also, maybe Password.Id.t rather than Password.Name.t

Making the password mutable means it can't easily cross contention, though.

We can just assert that it does. You can see it is semantically fine because the mutable part could be a ref inside the capsule the password is associated with, so that the password itself constituted permission to access it. It's just that we can't use the Password API inside the definition of the Password API.

What about shared passwords?

Yeah, due to val shared : 'k t @ local -> 'k Shared.t @ local @@ portable we have to use the atomic everywhere (and we need that function to write interfaces general over whether your data is guarded by a mutex or by a rw-lock).

I guess, we could track whether the shared password is sourced from a normal password or created shared, but that seems overly complicated.

Actually, it's pretty easy to track, so why not.

I wasn’t going to bother storing the atomic in the locks, my suggestion was to have ids only be the ids of passwords not of capsules generally, so we’d just stack allocate a fresh atomic cell for each new password.

I see. It feels somewhat wrong that just locking a mutex would require a new allocation. I guess we can compensate by adding another version of with_lock that provides Access.t instead.

otherlibs/stdlib_alpha/capsule.ml

testsuite/tests/capsule-api/key.ml

dkalinichenko-js · 2025-01-21T18:42:29Z

Updated to support Capsule.Key.with_password_local, removed redundant Capsule.Key.with_password{,_local} functions.

dkalinichenko-js · 2025-01-21T21:10:46Z

Updated to only initialize passwords on Password.name t. Both normal and shared passwords are backed by the same type, but normal passwords use unsynced access operations while shared passwords use atomics.

dkalinichenko-js · 2025-01-25T03:09:38Z

Updated the API to handle shared keys, Data.Shared, and freezing rw-locks. The diff is quite large, so I recommend reviewing this from the beginning.

lpw25

I've reviewed everything except the new tests. Will review them later/tomorrow.

otherlibs/stdlib_alpha/capsule.mli

lpw25 · 2025-02-11T13:23:10Z

otherlibs/stdlib_alpha/capsule.mli

-
-val create_with_rwlock : unit -> Rwlock.packed @@ portable
-(** [create_with_rwlock ()] creates a new capsule with an associated reader-writer lock. *)
-


I think it is probably still worth leaving these in as convenience functions.

I'll add them to the version in the tree.

lpw25 · 2025-02-11T17:12:36Z

otherlibs/stdlib_alpha/capsule.ml

+  let[@inline] with_password (type k) k f =
+    let pw : k Password.t = Password.unsafe_mk () in
+    try f pw, k with
+    | Encapsulated (id, data) as exn ->


I guess this should also catch Encapsulated_shared since the password might get converted to a shared password. The docs should also be updated to reflect this.

Removed shared instead, since it's either useless or unsound in presence of fork_join.

lpw25 · 2025-02-11T17:16:04Z

otherlibs/stdlib_alpha/capsule.ml

        | x -> Rw.unlock t.rwlock; x
        | exception exn ->
-          t.poisoned <- true;
+          t.state <- Frozen;


This needs to set it to Posioned rather than Frozen as the exception that is being leaked may mutate the data from the capsule.

lpw25 · 2025-02-11T17:17:15Z

otherlibs/stdlib_alpha/capsule.ml

        | x -> Rw.unlock t.rwlock; x
        | exception exn ->
-          (* Here we are not poisoning the RwLock, see [capsule.mli] for explanation *)
+          let exn =


Why is this done before releasing the lock here, but after releasing the lock in with_lock?

Inconsistently copied from Mutex. I think it is a mistake to do it after releasing the lock: there may be another exception raised that modifies the data in the capsule. I changed all functions to convert the exception before the lock is released.

lpw25 · 2025-02-11T17:26:42Z

otherlibs/stdlib_alpha/capsule.ml

+               | None -> exn)
+            | _ -> exn
+          in
+          t.state <- Frozen;


It is probably worth adding a comment here about why this racy write is ok according to the memory model. The reason it is ok is that:

All threads which race to write here are all racing to write Frozen and the only other write to this field in the program was the initial one that set it to Open.

All threads which race to read here do not distinguish between Open and Frozen so do not care which value they see.

The only reads which do care about the difference between Open and Frozen are ones that happen whilst holding the lock for writing -- that means there is a happens before relationship between them and all the writes, so they will reliably see the Frozen state.

Added a comment.

lpw25 · 2025-02-11T17:27:46Z

otherlibs/stdlib_alpha/capsule.ml

-    | false ->
-      t.poisoned <- true;
+      raise Poisoned
+    | Open | Frozen ->


This should fail with raise Frozen if the lock was already frozen. You cannot safely transition from Frozen to Poisoned.

dkalinichenko-js requested a review from lpw25 January 17, 2025 00:07

lpw25 reviewed Jan 17, 2025

View reviewed changes

dkalinichenko-js added the drf Data race freedom label Jan 17, 2025

dkalinichenko-js force-pushed the dkalinichenko/key-api branch from 93b7ee8 to 0fe9579 Compare January 25, 2025 03:07

dkalinichenko-js force-pushed the dkalinichenko/key-api branch from 86c2bf3 to 30c20c5 Compare February 3, 2025 17:24

lpw25 reviewed Feb 11, 2025

View reviewed changes

d-kalinichenko added 3 commits February 11, 2025 14:24

Key API

cb6b58a

Tests

3941d2f

fixes

d024d09

dkalinichenko-js force-pushed the dkalinichenko/key-api branch from 30c20c5 to d024d09 Compare February 11, 2025 20:06

d-kalinichenko added 3 commits February 11, 2025 15:10

fix

0d420d5

fix

db8a128

locally allocate atomics

5a0f68c

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Basic Key API #3485

Basic Key API #3485

dkalinichenko-js commented Jan 17, 2025

lpw25 left a comment

lpw25 Jan 17, 2025

lpw25 Jan 17, 2025

dkalinichenko-js Jan 17, 2025

lpw25 Jan 17, 2025

dkalinichenko-js Jan 17, 2025

dkalinichenko-js Jan 21, 2025

dkalinichenko-js Jan 21, 2025

dkalinichenko-js Jan 21, 2025

lpw25 Jan 22, 2025

dkalinichenko-js Jan 22, 2025

dkalinichenko-js commented Jan 21, 2025

dkalinichenko-js commented Jan 21, 2025

dkalinichenko-js commented Jan 25, 2025

lpw25 left a comment

lpw25 Feb 11, 2025

dkalinichenko-js Feb 11, 2025

lpw25 Feb 11, 2025

dkalinichenko-js Feb 11, 2025

lpw25 Feb 11, 2025

dkalinichenko-js Feb 11, 2025

lpw25 Feb 11, 2025

dkalinichenko-js Feb 11, 2025

lpw25 Feb 11, 2025

dkalinichenko-js Feb 11, 2025

lpw25 Feb 11, 2025

dkalinichenko-js Feb 11, 2025


		val create_with_rwlock : unit -> Rwlock.packed @@ portable
		(** [create_with_rwlock ()] creates a new capsule with an associated reader-writer lock. *)

Basic Key API #3485

Are you sure you want to change the base?

Basic Key API #3485

Conversation

dkalinichenko-js commented Jan 17, 2025

lpw25 left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

dkalinichenko-js commented Jan 21, 2025

dkalinichenko-js commented Jan 21, 2025

dkalinichenko-js commented Jan 25, 2025

lpw25 left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment