introduce shlease

book/src/dyn_tutorial/any.md

@@ -1,5 +1,7 @@
 # The `any` permission
 
+{{#include ../caveat.md}}
+
 Rather than labeling variables as `my` or `our`, you can also use the `any` keyword. This will permit the variable to store an object with any permission. When using `any`, the `give` and `share` keywords allow you to control the ownership:
 
 ```

book/src/permissions.md

@@ -6,10 +6,10 @@ Every reference to a Dada object has an associated **permission**. Each permissi
 
 Dada has four kinds of permissions, and they can be categorized along two dimensions:
 
-|        | Exclusive | Shared     |
-| ------ | --------- | ---------- |
-| Owned  | my        | our        |
-| Leased | leased    | our leased |
+|        | Exclusive | Shared   |
+| ------ | --------- | -------- |
+| Owned  | my        | our      |
+| Leased | leased    | shleased |
 
 **Exclusive permissions** give exclusive access to the object, meaning that while that permission is active, no other permission gives access to the same data. They give full ability to mutate. Exclusive permissions cannot be duplicated, but they can be *leased*, as will be discussed shortly. **Shared permissions** do not guarantee exclusive access. They can be freely duplicated.
 
@@ -35,9 +35,9 @@ The final point is interesting: we can have an `our` object (shared ownership) t
 class Point()
 
 fn test() -> {
-    p = Point().share        # our Point
-    q = p.lease              # our leased Point
-    q                        # returning to the caller drops `p`, cancelling `q`
+    any p = Point().share        # our Point
+    any q = p.lease              # shleased Point
+    q                            # returning to the caller drops `p`, cancelling `q`
 }
 
 fn main() {

components/dada-brew/src/brew.rs

@@ -164,6 +164,7 @@ impl Cursor {
             | validated::ExprData::Reserve(_)
             | validated::ExprData::Share(_)
             | validated::ExprData::Lease(_)
+            | validated::ExprData::Shlease(_)
             | validated::ExprData::Give(_)
             | validated::ExprData::Tuple(_)
             | validated::ExprData::Atomic(_) => {
@@ -290,6 +291,13 @@ impl Cursor {
                 self.push_breakpoint_ends(brewery, Some(target), origins, origin);
             }
 
+            validated::ExprData::Shlease(place) => {
+                let (place, origins) = self.brew_place(brewery, *place);
+                self.push_breakpoint_starts(brewery, origins.iter().copied(), origin);
+                self.push_assignment(brewery, target, bir::ExprData::Shlease(place), origin);
+                self.push_breakpoint_ends(brewery, Some(target), origins, origin);
+            }
+
             validated::ExprData::Give(place) => {
                 let (place, origins) = self.brew_place(brewery, *place);
                 self.push_breakpoint_starts(brewery, origins.iter().copied(), origin);

components/dada-execute/src/heap_graph.rs

@@ -143,7 +143,7 @@ pub(crate) enum PermissionNodeLabel {
     My,
     Our,
     Leased,
-    OurLeased,
+    Shleased,
     Reserved,
     Expired,
 }
@@ -154,7 +154,7 @@ impl PermissionNodeLabel {
             PermissionNodeLabel::My => "my",
             PermissionNodeLabel::Our => "our",
             PermissionNodeLabel::Leased => "leased",
-            PermissionNodeLabel::OurLeased => "our leased",
+            PermissionNodeLabel::Shleased => "shleased",
             PermissionNodeLabel::Reserved => "reserved",
             PermissionNodeLabel::Expired => "expired",
         }

components/dada-execute/src/heap_graph/capture.rs

@@ -159,7 +159,7 @@ impl<'me> HeapGraphCapture<'me> {
                 (Joint::No, Leased::No) => PermissionNodeLabel::My,
                 (Joint::Yes, Leased::No) => PermissionNodeLabel::Our,
                 (Joint::No, Leased::Yes) => PermissionNodeLabel::Leased,
-                (Joint::Yes, Leased::Yes) => PermissionNodeLabel::OurLeased,
+                (Joint::Yes, Leased::Yes) => PermissionNodeLabel::Shleased,
             },
         };
 

components/dada-execute/src/heap_graph/graphviz.rs

@@ -151,12 +151,12 @@ impl HeapGraph {
                 PermissionNodeLabel::Reserved => ("1.0", "odot"),
                 PermissionNodeLabel::Expired
                 | PermissionNodeLabel::Leased
-                | PermissionNodeLabel::OurLeased => ("1.0", "empty"),
+                | PermissionNodeLabel::Shleased => ("1.0", "empty"),
             };
 
             let color = match permission_data.label {
                 PermissionNodeLabel::My | PermissionNodeLabel::Leased => "red",
-                PermissionNodeLabel::OurLeased | PermissionNodeLabel::Our => "blue",
+                PermissionNodeLabel::Shleased | PermissionNodeLabel::Our => "blue",
                 PermissionNodeLabel::Reserved => "grey",
                 PermissionNodeLabel::Expired => "grey",
             };

components/dada-execute/src/machine.rs

@@ -495,7 +495,7 @@ impl ValidPermissionData {
             (Joint::No, Leased::No) => "my",
             (Joint::No, Leased::Yes) => "leased",
             (Joint::Yes, Leased::No) => "our",
-            (Joint::Yes, Leased::Yes) => "our leased",
+            (Joint::Yes, Leased::Yes) => "shleased",
         }
     }
 }

components/dada-execute/src/machine/stringify.rs

@@ -87,7 +87,7 @@ pub(crate) impl<T: ?Sized + MachineOp> DefaultStringify for T {
                 (Joint::No, Leased::No) => "my",
                 (Joint::Yes, Leased::No) => "our",
                 (Joint::No, Leased::Yes) => "leased",
-                (Joint::Yes, Leased::Yes) => "our leased",
+                (Joint::Yes, Leased::Yes) => "shleased",
             }),
         }
     }

components/dada-execute/src/step.rs

@@ -41,6 +41,7 @@ mod lease;
 mod reserve;
 mod revoke;
 mod share;
+mod shlease;
 mod tenant;
 mod traversal;
 
@@ -286,7 +287,7 @@ impl<'me> Stepper<'me> {
             Specifier::My => self.give_place(table, source_place)?,
             Specifier::Our => self.share_place(table, source_place)?,
             Specifier::Leased => self.lease_place(table, source_place)?,
-            Specifier::OurLeased => self.share_leased_place(table, source_place)?,
+            Specifier::Shleased => self.shlease_place(table, source_place)?,
             Specifier::Any => self.give_place(table, source_place)?,
         };
 
@@ -534,6 +535,7 @@ impl<'me> Stepper<'me> {
             bir::ExprData::Reserve(place) => self.reserve_place(table, *place),
             bir::ExprData::Share(place) => self.share_place(table, *place),
             bir::ExprData::Lease(place) => self.lease_place(table, *place),
+            bir::ExprData::Shlease(place) => self.shlease_place(table, *place),
             bir::ExprData::Give(place) => self.give_place(table, *place),
             bir::ExprData::Tuple(places) => {
                 let fields = places

components/dada-execute/src/step/lease.rs

@@ -13,10 +13,10 @@ impl Stepper<'_> {
     ///
     /// # Examples
     ///
-    /// Creates a shared point:
+    /// Creates a leased point:
     ///
     /// ```notrust
-    /// p = Point(22, 44).share
+    /// p = Point(22, 44).lease
     /// ```
     ///
     /// # Invariants
@@ -28,7 +28,7 @@ impl Stepper<'_> {
     ///   * If `place` is jointly accessible, result will be jointly accessible
     ///   * If `place` is exclusive, result will be exclusive
     /// * `place` remains valid and unchanged; asserting `place` or invalidating
-    ///   it may invalidate the result
+    ///   it may invalidate the result `v`.
     #[tracing::instrument(level = "Debug", skip(self, table))]
     pub(super) fn lease_place(
         &mut self,
@@ -116,28 +116,28 @@ impl Stepper<'_> {
         //                   :
         //                   : tenant
         //                   v
-        //                 --shared--> b
+        //                 --leased--> b
         //                 =========== resulting permission
         // ```
         //
         // ```notrust
         // a -my-> [ Obj ]
-        //         [  f  ] --leased---> b
+        //         [  f  ] --leased----> b
         //                   :
         //                   : tenant
         //                   v
-        //                 --shared--> b
-        //                 =========== resulting permission
+        //                 --leased----> b
+        //                 ============= resulting permission
         // ```
         //
         // ```notrust
         // a -our-> [ Obj ]
-        //          [  f  ] --leased---> b
+        //          [  f  ] --leased----> b
         //                    :
         //                    : tenant
         //                    v
-        //                  --shared--> b
-        //                  =========== resulting permission
+        //                  --shleased--> b
+        //                  ============= resulting permission
         // ```
         //
         // In each case, reasserting `a.f` *may* invalidate the resulting

components/dada-execute/src/step/revoke.rs

@@ -53,7 +53,7 @@ impl Stepper<'_> {
             return true;
         }
 
-        valid.tenants.iter().any(|p| self.is_sharing_access(*p))
+        false
     }
 
     #[tracing::instrument(level = "Debug", skip(self))]

components/dada-execute/src/step/share.rs

@@ -25,7 +25,8 @@ impl Stepper<'_> {
     /// * The result is shared
     /// * The shared result has the same ownership/lease properties as original path:
     ///   * If original path was owned, shared result is owned (sharing a `my Foo` gives an `our Foo`).
-    ///   * If original path was leased, shared result is leased and lives as long as original lease would (sharing a `my leased(p) Foo` gives an `our leased(p) Foo`).
+    ///   * If original path was leased, shared result is leased and lives as long as original lease would
+    ///     (sharing a `leased(p) Foo` gives a `shleased(p) Foo`).
     /// * After sharing, the original path can be read (or shared again) without disturbing the share.
     ///
     /// Implication:
@@ -42,36 +43,6 @@ impl Stepper<'_> {
         self.share_traversal(object_traversal)
     }
 
-    /// Equivalent to `foo.lease.share`, used when assigning to an `our shared` location.
-    #[tracing::instrument(level = "Debug", skip(self, table))]
-    pub(super) fn share_leased_place(
-        &mut self,
-        table: &bir::Tables,
-        place: bir::Place,
-    ) -> eyre::Result<Value> {
-        let object_traversal = self.traverse_to_object(table, place)?;
-        let object_traversal = self.confirm_reservation_if_any(table, object_traversal)?;
-        tracing::debug!(?object_traversal);
-        if let Joint::Yes = object_traversal.accumulated_permissions.joint {
-            self.lease_traversal(object_traversal)
-        } else if let Leased::Yes = object_traversal.accumulated_permissions.leased {
-            self.share_traversal(object_traversal)
-        } else {
-            // Fully owned: first lease it, which will create a new tenant.
-            let Value {
-                object,
-                permission: leased_permission,
-            } = self.lease_traversal(object_traversal)?;
-
-            // Then create a shared sublease of `permission`.
-            let shared_permission = self.new_tenant_permission(Joint::Yes, leased_permission);
-            Ok(Value {
-                object,
-                permission: shared_permission,
-            })
-        }
-    }
-
     #[tracing::instrument(level = "debug", skip(self))]
     pub(super) fn share_traversal(&mut self, traversal: ObjectTraversal) -> eyre::Result<Value> {
         // Sharing counts as a read of the data being shared.