From 4ff39bc2becaaa2c7cf8a14ec434f52b8b6b9e33 Mon Sep 17 00:00:00 2001 From: Niko Matsakis Date: Tue, 19 Apr 2022 06:20:29 -0400 Subject: [PATCH] introduce shlease --- book/src/dyn_tutorial/any.md | 2 + book/src/permissions.md | 14 +- components/dada-breakpoint/src/breakpoint.rs | 1 + components/dada-brew/src/brew.rs | 8 + components/dada-execute/src/heap_graph.rs | 4 +- .../dada-execute/src/heap_graph/capture.rs | 2 +- .../dada-execute/src/heap_graph/graphviz.rs | 4 +- components/dada-execute/src/machine.rs | 2 +- .../dada-execute/src/machine/stringify.rs | 2 +- components/dada-execute/src/step.rs | 4 +- components/dada-execute/src/step/lease.rs | 20 +-- components/dada-execute/src/step/revoke.rs | 2 +- components/dada-execute/src/step/share.rs | 33 +--- components/dada-execute/src/step/shlease.rs | 147 ++++++++++++++++++ components/dada-ir/src/code/bir.rs | 4 + components/dada-ir/src/code/syntax.rs | 4 + components/dada-ir/src/code/validated.rs | 4 + components/dada-ir/src/kw.rs | 2 + components/dada-ir/src/storage.rs | 14 +- components/dada-parse/src/parser/code.rs | 4 + components/dada-parse/src/parser/parameter.rs | 29 +--- .../dada-validate/src/validate/validator.rs | 11 +- dada_tests/heap-graph/dag/HeapGraph-0.ref | 2 +- .../heap-graph/leased-point/HeapGraph-0.ref | 6 +- .../heap-graph/line-start/HeapGraph-1.ref | 2 +- .../nested-functions/HeapGraph-0.ref | 6 +- .../heap-graph/nested-points/HeapGraph-1.ref | 2 +- .../heap-graph/nested-points/HeapGraph-2.ref | 6 +- .../heap-graph/tutorial-1/HeapGraph-2.ref | 2 +- .../heap-graph/tutorial-1/HeapGraph-3.ref | 2 +- .../heap-graph/tutorial-1/HeapGraph-4.ref | 4 +- .../exhaustive/give-var-leased-shared.dada | 6 +- .../give-var-leased-shared/stdout.ref | 6 +- .../exhaustive/lease-var-lease-shared.dada | 6 +- .../lease-var-lease-shared/stdout.ref | 6 +- .../exhaustive/share-var-leased.dada | 2 +- .../exhaustive/share-var-leased/stdout.ref | 2 +- .../house-parties-are-not-enough.dada | 8 +- .../house-parties-are-not-enough/stdout.ref | 4 +- ...se-parties-are-not-fair-to-the-tenant.dada | 7 +- .../permissions/revokation/house-party.dada | 23 --- .../revokation/house-party/stdout.ref | 3 - .../revokation/lease-vs-shlease-1.dada | 9 ++ .../compiler-output.ref | 0 .../revokation/lease-vs-shlease-1/stdout.ref | 1 + .../revokation/lease-vs-shlease-2.dada | 8 + .../lease-vs-shlease-2}/compiler-output.ref | 0 .../revokation/lease-vs-shlease-2/stdout.ref | 2 + .../revokation/overwrite-lease-share.dada | 2 +- .../overwrite-lease-share/stdout.ref | 2 +- .../our-to-our-leased-assign-field.dada | 2 +- .../our-to-our-leased-assign.dada | 2 +- .../reservations/our-to-our-leased-field.dada | 2 +- .../reservations/our-to-our-leased-var.dada | 2 +- ...sed-from-shared-rvalue-assign-in-loop.dada | 2 +- ...leased.dada => need-any-got-shleased.dada} | 0 .../compiler-output.ref | 0 .../stdout.ref | 0 ...sed.dada => need-leased-got-shleased.dada} | 0 .../compiler-output.ref | 0 .../stdout.ref | 0 ...-leased.dada => need-my-got-shleased.dada} | 0 .../compiler-output.ref | 0 .../stdout.ref | 0 ...leased.dada => need-our-got-shleased.dada} | 0 .../compiler-output.ref | 0 .../stdout.ref | 0 .../need-our-leased-got-our-leased.dada | 5 - ...our.dada => need-shleased-got-leased.dada} | 2 +- .../compiler-output.ref | 0 .../stdout.ref | 0 ...-got-my.dada => need-shleased-got-my.dada} | 2 +- .../compiler-output.ref | 0 .../stdout.ref | 0 ...leased.dada => need-shleased-got-our.dada} | 2 +- .../compiler-output.ref | 0 .../stdout.ref | 0 .../specifier/need-shleased-got-shleased.dada | 5 + .../compiler-output.ref | 0 .../need-shleased-got-shleased/stdout.ref | 0 .../our-lease-does-not-yield-leased.dada | 9 ++ .../compiler-output.ref | 0 .../stdout.ref | 0 .../specifier/our-lease-yields-our.dada | 10 ++ .../our-lease-yields-our/compiler-output.ref | 0 .../specifier/our-lease-yields-our/stdout.ref | 0 .../our-leased-got-my-then-copy.dada | 7 - .../our-leased-got-my-then-copy/stdout.ref | 1 - .../specifier/our-shlease-yields-our.dada | 10 ++ .../compiler-output.ref | 0 .../our-shlease-yields-our/stdout.ref | 0 ...ed-from-shared-rvalue-assign-in-loop.dada} | 2 +- .../compiler-output.ref | 0 .../stdout.ref | 0 .../specifier/shleased-got-my-then-copy.dada | 12 ++ .../compiler-output.ref | 0 .../shleased-got-my-then-copy/stdout.ref | 1 + .../op-eq/lhs_shared_field_of_func_call.dada | 2 +- 98 files changed, 346 insertions(+), 180 deletions(-) create mode 100644 components/dada-execute/src/step/shlease.rs delete mode 100644 dada_tests/permissions/revokation/house-party.dada delete mode 100644 dada_tests/permissions/revokation/house-party/stdout.ref create mode 100644 dada_tests/permissions/revokation/lease-vs-shlease-1.dada rename dada_tests/permissions/revokation/{house-party => lease-vs-shlease-1}/compiler-output.ref (100%) create mode 100644 dada_tests/permissions/revokation/lease-vs-shlease-1/stdout.ref create mode 100644 dada_tests/permissions/revokation/lease-vs-shlease-2.dada rename dada_tests/{specifier/need-any-got-our-leased => permissions/revokation/lease-vs-shlease-2}/compiler-output.ref (100%) create mode 100644 dada_tests/permissions/revokation/lease-vs-shlease-2/stdout.ref rename dada_tests/specifier/{need-any-got-our-leased.dada => need-any-got-shleased.dada} (100%) rename dada_tests/specifier/{need-leased-got-our-leased => need-any-got-shleased}/compiler-output.ref (100%) rename dada_tests/specifier/{need-any-got-our-leased => need-any-got-shleased}/stdout.ref (100%) rename dada_tests/specifier/{need-leased-got-our-leased.dada => need-leased-got-shleased.dada} (100%) rename dada_tests/specifier/{need-my-got-our-leased => need-leased-got-shleased}/compiler-output.ref (100%) rename dada_tests/specifier/{need-leased-got-our-leased => need-leased-got-shleased}/stdout.ref (100%) rename dada_tests/specifier/{need-my-got-our-leased.dada => need-my-got-shleased.dada} (100%) rename dada_tests/specifier/{need-our-got-our-leased => need-my-got-shleased}/compiler-output.ref (100%) rename dada_tests/specifier/{need-my-got-our-leased => need-my-got-shleased}/stdout.ref (100%) rename dada_tests/specifier/{need-our-got-our-leased.dada => need-our-got-shleased.dada} (100%) rename dada_tests/specifier/{need-our-leased-got-leased => need-our-got-shleased}/compiler-output.ref (100%) rename dada_tests/specifier/{need-our-got-our-leased => need-our-got-shleased}/stdout.ref (100%) delete mode 100644 dada_tests/specifier/need-our-leased-got-our-leased.dada rename dada_tests/specifier/{need-our-leased-got-our.dada => need-shleased-got-leased.dada} (50%) rename dada_tests/specifier/{need-our-leased-got-my => need-shleased-got-leased}/compiler-output.ref (100%) rename dada_tests/specifier/{need-our-leased-got-leased => need-shleased-got-leased}/stdout.ref (100%) rename dada_tests/specifier/{need-our-leased-got-my.dada => need-shleased-got-my.dada} (55%) rename dada_tests/specifier/{need-our-leased-got-our-leased => need-shleased-got-my}/compiler-output.ref (100%) rename dada_tests/specifier/{need-our-leased-got-my => need-shleased-got-my}/stdout.ref (100%) rename dada_tests/specifier/{need-our-leased-got-leased.dada => need-shleased-got-our.dada} (50%) rename dada_tests/specifier/{our-leased-from-shared-rvalue-assign-in-loop => need-shleased-got-our}/compiler-output.ref (100%) rename dada_tests/specifier/{need-our-leased-got-our-leased => need-shleased-got-our}/stdout.ref (100%) create mode 100644 dada_tests/specifier/need-shleased-got-shleased.dada rename dada_tests/specifier/{our-leased-got-my-then-copy => need-shleased-got-shleased}/compiler-output.ref (100%) create mode 100644 dada_tests/specifier/need-shleased-got-shleased/stdout.ref create mode 100644 dada_tests/specifier/our-lease-does-not-yield-leased.dada create mode 100644 dada_tests/specifier/our-lease-does-not-yield-leased/compiler-output.ref create mode 100644 dada_tests/specifier/our-lease-does-not-yield-leased/stdout.ref create mode 100644 dada_tests/specifier/our-lease-yields-our.dada create mode 100644 dada_tests/specifier/our-lease-yields-our/compiler-output.ref create mode 100644 dada_tests/specifier/our-lease-yields-our/stdout.ref delete mode 100644 dada_tests/specifier/our-leased-got-my-then-copy.dada delete mode 100644 dada_tests/specifier/our-leased-got-my-then-copy/stdout.ref create mode 100644 dada_tests/specifier/our-shlease-yields-our.dada create mode 100644 dada_tests/specifier/our-shlease-yields-our/compiler-output.ref create mode 100644 dada_tests/specifier/our-shlease-yields-our/stdout.ref rename dada_tests/specifier/{our-leased-from-shared-rvalue-assign-in-loop.dada => shleased-from-shared-rvalue-assign-in-loop.dada} (93%) create mode 100644 dada_tests/specifier/shleased-from-shared-rvalue-assign-in-loop/compiler-output.ref rename dada_tests/specifier/{our-leased-from-shared-rvalue-assign-in-loop => shleased-from-shared-rvalue-assign-in-loop}/stdout.ref (100%) create mode 100644 dada_tests/specifier/shleased-got-my-then-copy.dada create mode 100644 dada_tests/specifier/shleased-got-my-then-copy/compiler-output.ref create mode 100644 dada_tests/specifier/shleased-got-my-then-copy/stdout.ref diff --git a/book/src/dyn_tutorial/any.md b/book/src/dyn_tutorial/any.md index 49ede37f..90699728 100644 --- a/book/src/dyn_tutorial/any.md +++ b/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: ``` diff --git a/book/src/permissions.md b/book/src/permissions.md index 236c09b9..ac114ad0 100644 --- a/book/src/permissions.md +++ b/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() { diff --git a/components/dada-breakpoint/src/breakpoint.rs b/components/dada-breakpoint/src/breakpoint.rs index 6eaf9157..84a23d7f 100644 --- a/components/dada-breakpoint/src/breakpoint.rs +++ b/components/dada-breakpoint/src/breakpoint.rs @@ -112,6 +112,7 @@ impl TreeTraversal<'_> { | syntax::ExprData::Dot(base_expr, _) | syntax::ExprData::Share(base_expr) | syntax::ExprData::Lease(base_expr) + | syntax::ExprData::Shlease(base_expr) | syntax::ExprData::Give(base_expr) | syntax::ExprData::Await(base_expr) | syntax::ExprData::Loop(base_expr) diff --git a/components/dada-brew/src/brew.rs b/components/dada-brew/src/brew.rs index 88548519..8c2ab946 100644 --- a/components/dada-brew/src/brew.rs +++ b/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); diff --git a/components/dada-execute/src/heap_graph.rs b/components/dada-execute/src/heap_graph.rs index d6cf2095..f126f32c 100644 --- a/components/dada-execute/src/heap_graph.rs +++ b/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", } diff --git a/components/dada-execute/src/heap_graph/capture.rs b/components/dada-execute/src/heap_graph/capture.rs index 770ef024..1965abd4 100644 --- a/components/dada-execute/src/heap_graph/capture.rs +++ b/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, }, }; diff --git a/components/dada-execute/src/heap_graph/graphviz.rs b/components/dada-execute/src/heap_graph/graphviz.rs index 590684e6..8bc5dc4d 100644 --- a/components/dada-execute/src/heap_graph/graphviz.rs +++ b/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", }; diff --git a/components/dada-execute/src/machine.rs b/components/dada-execute/src/machine.rs index fb72a3f4..c4ef4877 100644 --- a/components/dada-execute/src/machine.rs +++ b/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", } } } diff --git a/components/dada-execute/src/machine/stringify.rs b/components/dada-execute/src/machine/stringify.rs index 820e4adb..f53bb997 100644 --- a/components/dada-execute/src/machine/stringify.rs +++ b/components/dada-execute/src/machine/stringify.rs @@ -87,7 +87,7 @@ pub(crate) impl 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", }), } } diff --git a/components/dada-execute/src/step.rs b/components/dada-execute/src/step.rs index 90b685b4..884516a1 100644 --- a/components/dada-execute/src/step.rs +++ b/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 diff --git a/components/dada-execute/src/step/lease.rs b/components/dada-execute/src/step/lease.rs index 261771d6..8eb99608 100644 --- a/components/dada-execute/src/step/lease.rs +++ b/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 diff --git a/components/dada-execute/src/step/revoke.rs b/components/dada-execute/src/step/revoke.rs index 139cb872..4d171978 100644 --- a/components/dada-execute/src/step/revoke.rs +++ b/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))] diff --git a/components/dada-execute/src/step/share.rs b/components/dada-execute/src/step/share.rs index 24930ad6..4640bd81 100644 --- a/components/dada-execute/src/step/share.rs +++ b/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 { - 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 { // Sharing counts as a read of the data being shared. diff --git a/components/dada-execute/src/step/shlease.rs b/components/dada-execute/src/step/shlease.rs new file mode 100644 index 00000000..72fdf47f --- /dev/null +++ b/components/dada-execute/src/step/shlease.rs @@ -0,0 +1,147 @@ +use dada_ir::{ + code::bir, + storage::{Joint, Leased}, +}; + +use crate::machine::{ValidPermissionData, Value}; + +use super::{traversal::ObjectTraversal, Stepper}; + +impl Stepper<'_> { + /// Shleasing an object creates a new permission that remains valid so long as the + /// original reference is not used to do a write. + /// + /// # Examples + /// + /// Creates a shleased point: + /// + /// ```notrust + /// p = Point(22, 44).shlease + /// ``` + /// + /// # Invariants + /// + /// The following invariants are maintained: + /// + /// * Results in a value `v` that refers to the same object as `place` + /// * Always returns a shared value + /// * `place` may be used for reads without invalidating the resulting value `v` + /// * `place` remains valid and unchanged; writing to `place` may invalidate the result `v`. + #[tracing::instrument(level = "Debug", skip(self, table))] + pub(super) fn shlease_place( + &mut self, + table: &bir::Tables, + place: bir::Place, + ) -> eyre::Result { + let object_traversal = self.traverse_to_object(table, place)?; + let object_traversal = self.confirm_reservation_if_any(table, object_traversal)?; + self.shlease_traversal(object_traversal) + } + + #[tracing::instrument(level = "Debug", skip(self))] + pub(super) fn shlease_traversal( + &mut self, + object_traversal: ObjectTraversal, + ) -> eyre::Result { + // Shleasing something is akin to reading it. + self.read(&object_traversal)?; + + let ObjectTraversal { + object, + accumulated_permissions, + } = object_traversal; + + // The last traversed permission is the one that led to the object + // (and there must be one, because you can't reach an object without + // traversing at least one permission). + let last_permission = *accumulated_permissions.traversed.last().unwrap(); + + // Special case: If last permission is already shared, we can just duplicate it + // + // # Example + // + // ```notrust + // a ----> [ Obj ] + // ===== [ f ] --shared---> b + // | ============ duplicate this permission + // can be any + // permission(s) + // ``` + // + // # Discussion + // + // Maintains our invariants: + // + // * Result is leased. + // * Preserves sharing properties. + // * `place` is not altered. + if let ValidPermissionData { + joint: Joint::Yes, .. + } = self.machine[last_permission].assert_valid() + { + return Ok(Value { + object, + permission: last_permission, + }); + } + + // If the input is `our`, clone it. Note that this preserves all the invariants, + // even though it results in an owned value. + if let (Joint::Yes, Leased::No) = ( + accumulated_permissions.joint, + accumulated_permissions.leased, + ) { + let permission = self.machine.new_permission(ValidPermissionData::our()); + return Ok(Value { object, permission }); + } + + // Otherwise, allocate a new joint lease permission. + // + // ## Examples + // + // In each case, we share `a.f`... + // + // ```notrust + // a -my-> [ Obj ] + // [ f ] --my--------> b + // : + // : tenant + // v + // --shleased--> b + // =========== resulting permission + // ``` + // + // ```notrust + // a -my-> [ Obj ] + // [ f ] --leased---> b + // : + // : tenant + // v + // --shleased--> b + // ============= resulting permission + // ``` + // + // ```notrust + // a -our-> [ Obj ] + // [ f ] --leased----> b + // : + // : tenant + // v + // --shleased--> b + // ============= resulting permission + // ``` + // + // In each case, writing through `a.f` *may* invalidate the resulting + // permission. + // + // # Discussion + // + // Maintains our invariants: + // + // * Result is shleased. + // * Permissions for `place` are never altered. + let permission = self.new_tenant_permission(Joint::Yes, last_permission); + + Ok(Value { object, permission }) + } +} diff --git a/components/dada-ir/src/code/bir.rs b/components/dada-ir/src/code/bir.rs index ae58b467..fce555a3 100644 --- a/components/dada-ir/src/code/bir.rs +++ b/components/dada-ir/src/code/bir.rs @@ -427,6 +427,9 @@ pub enum ExprData { /// `expr.lease` Lease(Place), + /// `expr.shlease` + Shlease(Place), + /// `expr.give` Give(Place), @@ -458,6 +461,7 @@ impl DebugWithDb> for ExprData { ExprData::Reserve(p) => write!(f, "{:?}.reserve", p.debug(db)), ExprData::Share(p) => write!(f, "{:?}.share", p.debug(db)), ExprData::Lease(p) => write!(f, "{:?}.lease", p.debug(db)), + ExprData::Shlease(p) => write!(f, "{:?}.shlease", p.debug(db)), ExprData::Give(p) => write!(f, "{:?}.give", p.debug(db)), ExprData::Unit => write!(f, "()"), ExprData::Tuple(vars) => write_parenthesized_places(f, vars, db), diff --git a/components/dada-ir/src/code/syntax.rs b/components/dada-ir/src/code/syntax.rs index a7e0d676..8d68c039 100644 --- a/components/dada-ir/src/code/syntax.rs +++ b/components/dada-ir/src/code/syntax.rs @@ -124,6 +124,9 @@ pub enum ExprData { /// `expr.lease` Lease(Expr), + /// `expr.shlease` + Shlease(Expr), + /// `expr.give` Give(Expr), @@ -196,6 +199,7 @@ impl DebugWithDb> for ExprData { .finish(), ExprData::Share(e) => f.debug_tuple("Share").field(&e.debug(db)).finish(), ExprData::Lease(e) => f.debug_tuple("Lease").field(&e.debug(db)).finish(), + ExprData::Shlease(e) => f.debug_tuple("Shlease").field(&e.debug(db)).finish(), ExprData::Give(e) => f.debug_tuple("Give").field(&e.debug(db)).finish(), ExprData::Var(v, e) => f .debug_tuple("Var") diff --git a/components/dada-ir/src/code/validated.rs b/components/dada-ir/src/code/validated.rs index af34b126..c9245e7d 100644 --- a/components/dada-ir/src/code/validated.rs +++ b/components/dada-ir/src/code/validated.rs @@ -252,6 +252,9 @@ pub enum ExprData { /// `expr.lease` Lease(Place), + /// `expr.shlease` + Shlease(Place), + /// `expr.give` Give(Place), @@ -339,6 +342,7 @@ impl ExprData { ExprData::Reserve(p) => f.debug_tuple("Reserve").field(&p.debug(db)).finish(), ExprData::Share(p) => f.debug_tuple("Share").field(&p.debug(db)).finish(), ExprData::Lease(p) => f.debug_tuple("Lease").field(&p.debug(db)).finish(), + ExprData::Shlease(p) => f.debug_tuple("Shlease").field(&p.debug(db)).finish(), ExprData::Give(p) => f.debug_tuple("Give").field(&p.debug(db)).finish(), ExprData::Tuple(exprs) => { let mut f = f.debug_tuple("Tuple"); diff --git a/components/dada-ir/src/kw.rs b/components/dada-ir/src/kw.rs index 55990eb8..7c4cf074 100644 --- a/components/dada-ir/src/kw.rs +++ b/components/dada-ir/src/kw.rs @@ -60,6 +60,8 @@ define_keywords! { Return => "return", Share => "share", Shared => "shared", + Shlease => "shlease", + Shleased => "shleased", True => "true", Our => "our", While => "while", diff --git a/components/dada-ir/src/storage.rs b/components/dada-ir/src/storage.rs index 095c9868..50dcc20f 100644 --- a/components/dada-ir/src/storage.rs +++ b/components/dada-ir/src/storage.rs @@ -19,7 +19,7 @@ impl SpannedSpecifier { /// Creates a new `SpannedSpecifier` for a variable/field that didn't /// have an explicit specifier. pub fn new_defaulted(db: &dyn crate::Db, name_span: FileSpan) -> Self { - Self::new(db, Specifier::OurLeased, true, name_span) + Self::new(db, Specifier::Shleased, true, name_span) } } @@ -28,31 +28,31 @@ pub enum Specifier { My, Our, Leased, - OurLeased, + Shleased, Any, } impl Specifier { /// True if values stored under this specifier must be uniquely - /// accessible (my, leased) and cannot be jointly accessible (our, our leased). + /// accessible (my, leased) and cannot be jointly accessible (our, shleased). /// /// [`Specifier::Any`] returns false. pub fn must_be_unique(self) -> bool { match self { Specifier::My | Specifier::Leased => true, - Specifier::Our | Specifier::OurLeased => false, + Specifier::Our | Specifier::Shleased => false, Specifier::Any => false, } } /// True if values stored under this specifier must be owned (my, our) - /// and cannot be leased (leased, our leased). + /// and cannot be leased (leased, shleased). /// /// [`Specifier::Any`] returns false. pub fn must_be_owned(self) -> bool { match self { Specifier::Our | Specifier::My => true, - Specifier::OurLeased | Specifier::Leased => false, + Specifier::Shleased | Specifier::Leased => false, Specifier::Any => false, } } @@ -63,7 +63,7 @@ impl std::fmt::Display for Specifier { match self { Specifier::Our => write!(f, "our"), Specifier::My => write!(f, "my"), - Specifier::OurLeased => write!(f, "our leased"), + Specifier::Shleased => write!(f, "shleased"), Specifier::Leased => write!(f, "leased"), Specifier::Any => write!(f, "any"), } diff --git a/components/dada-parse/src/parser/code.rs b/components/dada-parse/src/parser/code.rs index 5ed6e5aa..9fd5c7af 100644 --- a/components/dada-parse/src/parser/code.rs +++ b/components/dada-parse/src/parser/code.rs @@ -305,6 +305,10 @@ impl CodeParser<'_, '_> { let span = self.spans[expr].to(kw_span); expr = self.add(ExprData::Lease(expr), span); continue; + } else if let Some((kw_span, _)) = self.eat(Keyword::Shlease) { + let span = self.spans[expr].to(kw_span); + expr = self.add(ExprData::Shlease(expr), span); + continue; } else { self.parser .error_at_current_token("expected identifier after `.`") diff --git a/components/dada-parse/src/parser/parameter.rs b/components/dada-parse/src/parser/parameter.rs index 997d0e2c..51945ff4 100644 --- a/components/dada-parse/src/parser/parameter.rs +++ b/components/dada-parse/src/parser/parameter.rs @@ -88,32 +88,13 @@ impl<'db> Parser<'db> { )) }; if let Some((my_span, _)) = self.eat(Keyword::My) { - if let Some((leased_span, _)) = self.eat(Keyword::Leased) { - some_specifier(Specifier::Leased, my_span.to(leased_span)) - } else { - some_specifier(Specifier::My, my_span) - } + some_specifier(Specifier::My, my_span) } else if let Some((our_span, _)) = self.eat(Keyword::Our) { - if let Some((leased_span, _)) = self.eat(Keyword::Leased) { - some_specifier(Specifier::OurLeased, our_span.to(leased_span)) - } else { - some_specifier(Specifier::Our, our_span) - } + some_specifier(Specifier::Our, our_span) + } else if let Some((shleased_span, _)) = self.eat(Keyword::Shleased) { + some_specifier(Specifier::Shleased, shleased_span) } else if let Some((leased_span, _)) = self.eat(Keyword::Leased) { - if let Some((my_span, _)) = self.eat(Keyword::My) { - self.error(my_span, "this should be written `leased`, not `leased my`") - .emit(self.db); - some_specifier(Specifier::Leased, leased_span.to(my_span)) - } else if let Some((our_span, _)) = self.eat(Keyword::Our) { - self.error( - our_span, - "this should be written `our leased`, not `leased our`", - ) - .emit(self.db); - some_specifier(Specifier::OurLeased, leased_span.to(our_span)) - } else { - some_specifier(Specifier::Leased, leased_span) - } + some_specifier(Specifier::Leased, leased_span) } else if let Some((any_span, _)) = self.eat(Keyword::Any) { some_specifier(Specifier::Any, any_span) } else { diff --git a/components/dada-validate/src/validate/validator.rs b/components/dada-validate/src/validate/validator.rs index 1df2afe6..223b1c43 100644 --- a/components/dada-validate/src/validate/validator.rs +++ b/components/dada-validate/src/validate/validator.rs @@ -338,6 +338,10 @@ impl<'me> Validator<'me> { self.validate_permission_expr(expr, *target_expr, validated::ExprData::Lease) } + syntax::ExprData::Shlease(target_expr) => { + self.validate_permission_expr(expr, *target_expr, validated::ExprData::Shlease) + } + syntax::ExprData::Give(target_expr) => { if self.is_place_expression(*target_expr) { self.validate_permission_expr(expr, *target_expr, validated::ExprData::Give) @@ -776,10 +780,9 @@ impl<'me> Validator<'me> { let shared_expr = self.add(validated::ExprData::Share(given_expr), origin); self.seq(opt_assign_expr, shared_expr) } - ExprMode::Specifier(Specifier::OurLeased) => { - let given_expr = self.add(validated::ExprData::Lease(place), origin); - let shared_expr = self.add(validated::ExprData::Share(given_expr), origin); - self.seq(opt_assign_expr, shared_expr) + ExprMode::Specifier(Specifier::Shleased) => { + let place_expr = self.add(validated::ExprData::Shlease(place), origin); + self.seq(opt_assign_expr, place_expr) } }, Err(ErrorReported) => self.add(validated::ExprData::Error, origin), diff --git a/dada_tests/heap-graph/dag/HeapGraph-0.ref b/dada_tests/heap-graph/dag/HeapGraph-0.ref index 0074a39d..138eef30 100644 --- a/dada_tests/heap-graph/dag/HeapGraph-0.ref +++ b/dada_tests/heap-graph/dag/HeapGraph-0.ref @@ -34,7 +34,7 @@ digraph { > ]; "afterstack":0 -> "afternode0" [label="our", style="solid", penwidth=3.0, arrowtype="normal", color="blue"]; - "afterstack":2 -> "afternode1" [label="our leased", style="solid", penwidth=1.0, arrowtype="empty", color="blue"]; + "afterstack":2 -> "afternode1" [label="shleased", style="solid", penwidth=1.0, arrowtype="empty", color="blue"]; "afternode1":0 -> "afternode0" [label="our", style="solid", penwidth=3.0, arrowtype="normal", color="blue"]; "afternode1":1 -> "afternode0" [label="our", style="solid", penwidth=3.0, arrowtype="normal", color="blue"]; } diff --git a/dada_tests/heap-graph/leased-point/HeapGraph-0.ref b/dada_tests/heap-graph/leased-point/HeapGraph-0.ref index fcf6b9d1..5ecf1320 100644 --- a/dada_tests/heap-graph/leased-point/HeapGraph-0.ref +++ b/dada_tests/heap-graph/leased-point/HeapGraph-0.ref @@ -33,9 +33,9 @@ digraph { y: "44" > ]; - "afterstack":0 -> "afternode0" [label="our leased", style="solid", penwidth=1.0, arrowtype="empty", color="blue"]; - "afterstack":2 -> "afternode1" [label="our leased", style="solid", penwidth=1.0, arrowtype="empty", color="blue"]; - "afternode1":0 -> "afternode0" [label="our leased", style="solid", penwidth=1.0, arrowtype="empty", color="blue"]; + "afterstack":0 -> "afternode0" [label="shleased", style="solid", penwidth=1.0, arrowtype="empty", color="blue"]; + "afterstack":2 -> "afternode1" [label="shleased", style="solid", penwidth=1.0, arrowtype="empty", color="blue"]; + "afternode1":0 -> "afternode0" [label="shleased", style="solid", penwidth=1.0, arrowtype="empty", color="blue"]; } subgraph cluster_before { label=<before> diff --git a/dada_tests/heap-graph/line-start/HeapGraph-1.ref b/dada_tests/heap-graph/line-start/HeapGraph-1.ref index e6c67792..f878b67a 100644 --- a/dada_tests/heap-graph/line-start/HeapGraph-1.ref +++ b/dada_tests/heap-graph/line-start/HeapGraph-1.ref @@ -27,7 +27,7 @@ digraph { y: "44" > ]; - "afterstack":0 -> "afternode0" [label="our leased", style="solid", penwidth=1.0, arrowtype="empty", color="blue"]; + "afterstack":0 -> "afternode0" [label="shleased", style="solid", penwidth=1.0, arrowtype="empty", color="blue"]; } subgraph cluster_before { label=<before> diff --git a/dada_tests/heap-graph/nested-functions/HeapGraph-0.ref b/dada_tests/heap-graph/nested-functions/HeapGraph-0.ref index be5c9a45..c24e5f66 100644 --- a/dada_tests/heap-graph/nested-functions/HeapGraph-0.ref +++ b/dada_tests/heap-graph/nested-functions/HeapGraph-0.ref @@ -37,9 +37,9 @@ digraph { y: "44" > ]; - "afterstack":14 -> "afternode0" [label="our leased", style="solid", penwidth=1.0, arrowtype="empty", color="blue"]; + "afterstack":14 -> "afternode0" [label="shleased", style="solid", penwidth=1.0, arrowtype="empty", color="blue"]; "stack":26 -> "afternode1" [label="my", style="solid", penwidth=3.0, arrowtype="normal", color="red"]; - "afternode1":0 -> "afternode0" [label="our leased", style="solid", penwidth=1.0, arrowtype="empty", color="blue"]; + "afternode1":0 -> "afternode0" [label="shleased", style="solid", penwidth=1.0, arrowtype="empty", color="blue"]; } subgraph cluster_before { label=<before> @@ -68,7 +68,7 @@ digraph { y: "44" > ]; - "beforestack":14 -> "beforenode0" [label="our leased", style="solid", penwidth=1.0, arrowtype="empty", color="blue"]; + "beforestack":14 -> "beforenode0" [label="shleased", style="solid", penwidth=1.0, arrowtype="empty", color="blue"]; } } Hello diff --git a/dada_tests/heap-graph/nested-points/HeapGraph-1.ref b/dada_tests/heap-graph/nested-points/HeapGraph-1.ref index bd1e0304..17b4fef8 100644 --- a/dada_tests/heap-graph/nested-points/HeapGraph-1.ref +++ b/dada_tests/heap-graph/nested-points/HeapGraph-1.ref @@ -27,7 +27,7 @@ digraph { y: "44" > ]; - "afterstack":0 -> "afternode0" [label="our leased", style="solid", penwidth=1.0, arrowtype="empty", color="blue"]; + "afterstack":0 -> "afternode0" [label="shleased", style="solid", penwidth=1.0, arrowtype="empty", color="blue"]; } subgraph cluster_before { label=<before> diff --git a/dada_tests/heap-graph/nested-points/HeapGraph-2.ref b/dada_tests/heap-graph/nested-points/HeapGraph-2.ref index b82e0acc..86d04585 100644 --- a/dada_tests/heap-graph/nested-points/HeapGraph-2.ref +++ b/dada_tests/heap-graph/nested-points/HeapGraph-2.ref @@ -28,8 +28,8 @@ digraph { y: "44" > ]; - "afterstack":0 -> "afternode0" [label="our leased", style="solid", penwidth=1.0, arrowtype="empty", color="blue"]; - "stack":12 -> "afternode0" [label="our leased", style="solid", penwidth=1.0, arrowtype="empty", color="blue"]; + "afterstack":0 -> "afternode0" [label="shleased", style="solid", penwidth=1.0, arrowtype="empty", color="blue"]; + "stack":12 -> "afternode0" [label="shleased", style="solid", penwidth=1.0, arrowtype="empty", color="blue"]; } subgraph cluster_before { label=<before> @@ -56,6 +56,6 @@ digraph { y: "44" > ]; - "beforestack":0 -> "beforenode0" [label="our leased", style="solid", penwidth=1.0, arrowtype="empty", color="blue"]; + "beforestack":0 -> "beforenode0" [label="shleased", style="solid", penwidth=1.0, arrowtype="empty", color="blue"]; } } diff --git a/dada_tests/heap-graph/tutorial-1/HeapGraph-2.ref b/dada_tests/heap-graph/tutorial-1/HeapGraph-2.ref index 4f8eaaa2..c73503ba 100644 --- a/dada_tests/heap-graph/tutorial-1/HeapGraph-2.ref +++ b/dada_tests/heap-graph/tutorial-1/HeapGraph-2.ref @@ -26,7 +26,7 @@ digraph { y: "44" > ]; - "afterstack":0 -> "afternode0" [label="our leased", style="solid", penwidth=1.0, arrowtype="empty", color="blue"]; + "afterstack":0 -> "afternode0" [label="shleased", style="solid", penwidth=1.0, arrowtype="empty", color="blue"]; } subgraph cluster_before { label=<before> diff --git a/dada_tests/heap-graph/tutorial-1/HeapGraph-3.ref b/dada_tests/heap-graph/tutorial-1/HeapGraph-3.ref index 4f8eaaa2..c73503ba 100644 --- a/dada_tests/heap-graph/tutorial-1/HeapGraph-3.ref +++ b/dada_tests/heap-graph/tutorial-1/HeapGraph-3.ref @@ -26,7 +26,7 @@ digraph { y: "44" > ]; - "afterstack":0 -> "afternode0" [label="our leased", style="solid", penwidth=1.0, arrowtype="empty", color="blue"]; + "afterstack":0 -> "afternode0" [label="shleased", style="solid", penwidth=1.0, arrowtype="empty", color="blue"]; } subgraph cluster_before { label=<before> diff --git a/dada_tests/heap-graph/tutorial-1/HeapGraph-4.ref b/dada_tests/heap-graph/tutorial-1/HeapGraph-4.ref index 0683cc4c..ae8ad811 100644 --- a/dada_tests/heap-graph/tutorial-1/HeapGraph-4.ref +++ b/dada_tests/heap-graph/tutorial-1/HeapGraph-4.ref @@ -27,7 +27,7 @@ digraph { y: "44" > ]; - "afterstack":0 -> "afternode0" [label="our leased", style="solid", penwidth=1.0, arrowtype="empty", color="blue"]; + "afterstack":0 -> "afternode0" [label="shleased", style="solid", penwidth=1.0, arrowtype="empty", color="blue"]; } subgraph cluster_before { label=<before> @@ -53,7 +53,7 @@ digraph { y: "44" > ]; - "beforestack":0 -> "beforenode0" [label="our leased", style="solid", penwidth=1.0, arrowtype="empty", color="blue"]; + "beforestack":0 -> "beforenode0" [label="shleased", style="solid", penwidth=1.0, arrowtype="empty", color="blue"]; } } The point is FIXME diff --git a/dada_tests/permissions/exhaustive/give-var-leased-shared.dada b/dada_tests/permissions/exhaustive/give-var-leased-shared.dada index 8f8705dd..8a3a6e88 100644 --- a/dada_tests/permissions/exhaustive/give-var-leased-shared.dada +++ b/dada_tests/permissions/exhaustive/give-var-leased-shared.dada @@ -4,7 +4,7 @@ async fn main() { # FIXME: Debatable when the underlying pair should be freed. p = Pair(22, 44).lease.share q = p.give - print(p).await #! OUTPUT our leased Pair\(22, 44\) - print(q).await #! OUTPUT our leased Pair\(22, 44\) - print(p).await #! OUTPUT our leased Pair\(22, 44\) + print(p).await #! OUTPUT shleased Pair\(22, 44\) + print(q).await #! OUTPUT shleased Pair\(22, 44\) + print(p).await #! OUTPUT shleased Pair\(22, 44\) } \ No newline at end of file diff --git a/dada_tests/permissions/exhaustive/give-var-leased-shared/stdout.ref b/dada_tests/permissions/exhaustive/give-var-leased-shared/stdout.ref index 45d73dc0..4e0602fe 100644 --- a/dada_tests/permissions/exhaustive/give-var-leased-shared/stdout.ref +++ b/dada_tests/permissions/exhaustive/give-var-leased-shared/stdout.ref @@ -1,3 +1,3 @@ -our leased Pair(22, 44) -our leased Pair(22, 44) -our leased Pair(22, 44) +shleased Pair(22, 44) +shleased Pair(22, 44) +shleased Pair(22, 44) diff --git a/dada_tests/permissions/exhaustive/lease-var-lease-shared.dada b/dada_tests/permissions/exhaustive/lease-var-lease-shared.dada index 1b26dfa1..19a60344 100644 --- a/dada_tests/permissions/exhaustive/lease-var-lease-shared.dada +++ b/dada_tests/permissions/exhaustive/lease-var-lease-shared.dada @@ -3,7 +3,7 @@ class Pair(any a, any b) async fn main() { p = Pair(22, 44).lease.share q = p.lease - print(q).await #! OUTPUT our leased Pair\(22, 44\) - print(p).await #! OUTPUT our leased Pair\(22, 44\) - print(q).await #! OUTPUT our leased Pair\(22, 44\) + print(q).await #! OUTPUT shleased Pair\(22, 44\) + print(p).await #! OUTPUT shleased Pair\(22, 44\) + print(q).await #! OUTPUT shleased Pair\(22, 44\) } \ No newline at end of file diff --git a/dada_tests/permissions/exhaustive/lease-var-lease-shared/stdout.ref b/dada_tests/permissions/exhaustive/lease-var-lease-shared/stdout.ref index 45d73dc0..4e0602fe 100644 --- a/dada_tests/permissions/exhaustive/lease-var-lease-shared/stdout.ref +++ b/dada_tests/permissions/exhaustive/lease-var-lease-shared/stdout.ref @@ -1,3 +1,3 @@ -our leased Pair(22, 44) -our leased Pair(22, 44) -our leased Pair(22, 44) +shleased Pair(22, 44) +shleased Pair(22, 44) +shleased Pair(22, 44) diff --git a/dada_tests/permissions/exhaustive/share-var-leased.dada b/dada_tests/permissions/exhaustive/share-var-leased.dada index 0906897e..da399fee 100644 --- a/dada_tests/permissions/exhaustive/share-var-leased.dada +++ b/dada_tests/permissions/exhaustive/share-var-leased.dada @@ -7,7 +7,7 @@ async fn main() { any q = p.share # Accessing `q`: ok - print(q).await #! OUTPUT our leased Pair\(22, 44\) + print(q).await #! OUTPUT shleased Pair\(22, 44\) # Accessing `p`: ok, but cancels subleases print(p).await #! OUTPUT leased Pair\(22, 44\) diff --git a/dada_tests/permissions/exhaustive/share-var-leased/stdout.ref b/dada_tests/permissions/exhaustive/share-var-leased/stdout.ref index 71906f6a..849915a3 100644 --- a/dada_tests/permissions/exhaustive/share-var-leased/stdout.ref +++ b/dada_tests/permissions/exhaustive/share-var-leased/stdout.ref @@ -1,2 +1,2 @@ -our leased Pair(22, 44) +shleased Pair(22, 44) leased Pair(22, 44) diff --git a/dada_tests/permissions/house-parties/house-parties-are-not-enough.dada b/dada_tests/permissions/house-parties/house-parties-are-not-enough.dada index a060ddc7..5ee319ad 100644 --- a/dada_tests/permissions/house-parties/house-parties-are-not-enough.dada +++ b/dada_tests/permissions/house-parties/house-parties-are-not-enough.dada @@ -7,6 +7,9 @@ class Accumulator(my list) class List() +# This function takes a `shleased` accumulator and returns a +# `shleased` result. (Though, if given an `our` accumulator, +# it will return an `our` list, given current rules.) fn get_list(accumulator) # -> { accumulator.list.share @@ -24,7 +27,6 @@ async fn main() { l1 = get_list(a) l2 = get_list(a) print(l2).await #! OUTPUT List\(\) - print(l1).await #! RUN ERROR your lease to this object was cancelled - print(l2).await - #! FIXME: House parties are not enough to express Rust patterns + print(l1).await #! OUTPUT shleased List + print(l2).await #! OUTPUT shleased List } diff --git a/dada_tests/permissions/house-parties/house-parties-are-not-enough/stdout.ref b/dada_tests/permissions/house-parties/house-parties-are-not-enough/stdout.ref index 81444e49..3a5f284d 100644 --- a/dada_tests/permissions/house-parties/house-parties-are-not-enough/stdout.ref +++ b/dada_tests/permissions/house-parties/house-parties-are-not-enough/stdout.ref @@ -1 +1,3 @@ -our leased List() +shleased List() +shleased List() +shleased List() diff --git a/dada_tests/permissions/house-parties/house-parties-are-not-fair-to-the-tenant.dada b/dada_tests/permissions/house-parties/house-parties-are-not-fair-to-the-tenant.dada index cb99a893..b0ea6075 100644 --- a/dada_tests/permissions/house-parties/house-parties-are-not-fair-to-the-tenant.dada +++ b/dada_tests/permissions/house-parties/house-parties-are-not-fair-to-the-tenant.dada @@ -11,15 +11,16 @@ # But I'm pretty sure it's there. class Accumulator(my atomic list) -class List() +class List(our field) -fn foo(leased accumulator) # -> +fn foo(leased accumulator) # -> shleased List { + #! FIXME: Reading an atomic field without atomic section should not be allowed accumulator.list.lease.share } async fn main() { - my a = Accumulator(list: List()) + my a = Accumulator(list: List(22)) # get a shared lease to the list, # but it is still owned by `a` diff --git a/dada_tests/permissions/revokation/house-party.dada b/dada_tests/permissions/revokation/house-party.dada deleted file mode 100644 index 760b72e9..00000000 --- a/dada_tests/permissions/revokation/house-party.dada +++ /dev/null @@ -1,23 +0,0 @@ -class Character(name) - -# Test the "house party" pattern, in which we -# lease out an object `owner` to create `lessee` -# and then share `lessee` to create `guest`. -# -# If there is a read through `owner`, does that -# need to cancel `lessee`? (Answer: no.) -# -# Same question for a read through `lessee` -- it does -# not need to cancel guest. - -async fn main() { - any owner = Character("Achilles") - any lessee = owner.lease - any guest = lessee.share - print(owner.name).await #! OUTPUT Achilles - print(lessee.name).await #! OUTPUT Achilles - print(guest.name).await #! OUTPUT Achilles - - owner.name := "Paris" - print(guest.name).await #! RUN ERROR your lease to this object was cancelled -} \ No newline at end of file diff --git a/dada_tests/permissions/revokation/house-party/stdout.ref b/dada_tests/permissions/revokation/house-party/stdout.ref deleted file mode 100644 index 45bab171..00000000 --- a/dada_tests/permissions/revokation/house-party/stdout.ref +++ /dev/null @@ -1,3 +0,0 @@ -Achilles -Achilles -Achilles diff --git a/dada_tests/permissions/revokation/lease-vs-shlease-1.dada b/dada_tests/permissions/revokation/lease-vs-shlease-1.dada new file mode 100644 index 00000000..86a9ae6b --- /dev/null +++ b/dada_tests/permissions/revokation/lease-vs-shlease-1.dada @@ -0,0 +1,9 @@ +class Data(our field) + +async fn main() { + my m = Data(22) + leased l = m + shleased s = l + print(m.field).await #! OUTPUT 22 + print(s.field).await #! RUN ERROR your lease to this object was cancelled +} diff --git a/dada_tests/permissions/revokation/house-party/compiler-output.ref b/dada_tests/permissions/revokation/lease-vs-shlease-1/compiler-output.ref similarity index 100% rename from dada_tests/permissions/revokation/house-party/compiler-output.ref rename to dada_tests/permissions/revokation/lease-vs-shlease-1/compiler-output.ref diff --git a/dada_tests/permissions/revokation/lease-vs-shlease-1/stdout.ref b/dada_tests/permissions/revokation/lease-vs-shlease-1/stdout.ref new file mode 100644 index 00000000..2bd5a0a9 --- /dev/null +++ b/dada_tests/permissions/revokation/lease-vs-shlease-1/stdout.ref @@ -0,0 +1 @@ +22 diff --git a/dada_tests/permissions/revokation/lease-vs-shlease-2.dada b/dada_tests/permissions/revokation/lease-vs-shlease-2.dada new file mode 100644 index 00000000..cf73d7b7 --- /dev/null +++ b/dada_tests/permissions/revokation/lease-vs-shlease-2.dada @@ -0,0 +1,8 @@ +class Data(our field) + +async fn main() { + my m = Data(22) + shleased s = m + print(m.field).await #! OUTPUT 22 + print(s.field).await #! OUTPUT 22 +} diff --git a/dada_tests/specifier/need-any-got-our-leased/compiler-output.ref b/dada_tests/permissions/revokation/lease-vs-shlease-2/compiler-output.ref similarity index 100% rename from dada_tests/specifier/need-any-got-our-leased/compiler-output.ref rename to dada_tests/permissions/revokation/lease-vs-shlease-2/compiler-output.ref diff --git a/dada_tests/permissions/revokation/lease-vs-shlease-2/stdout.ref b/dada_tests/permissions/revokation/lease-vs-shlease-2/stdout.ref new file mode 100644 index 00000000..463ab342 --- /dev/null +++ b/dada_tests/permissions/revokation/lease-vs-shlease-2/stdout.ref @@ -0,0 +1,2 @@ +22 +22 diff --git a/dada_tests/permissions/revokation/overwrite-lease-share.dada b/dada_tests/permissions/revokation/overwrite-lease-share.dada index 8cfa050d..eb7a37c9 100644 --- a/dada_tests/permissions/revokation/overwrite-lease-share.dada +++ b/dada_tests/permissions/revokation/overwrite-lease-share.dada @@ -8,5 +8,5 @@ async fn main() { pair2.a := Pair(23, 45) - print(p).await #! OUTPUT our leased Pair\(22, 44\) + print(p).await #! OUTPUT shleased Pair\(22, 44\) } \ No newline at end of file diff --git a/dada_tests/permissions/revokation/overwrite-lease-share/stdout.ref b/dada_tests/permissions/revokation/overwrite-lease-share/stdout.ref index 50c48401..cd1bd4b7 100644 --- a/dada_tests/permissions/revokation/overwrite-lease-share/stdout.ref +++ b/dada_tests/permissions/revokation/overwrite-lease-share/stdout.ref @@ -1 +1 @@ -our leased Pair(22, 44) +shleased Pair(22, 44) diff --git a/dada_tests/reservations/our-to-our-leased-assign-field.dada b/dada_tests/reservations/our-to-our-leased-assign-field.dada index c1fb2483..29825a01 100644 --- a/dada_tests/reservations/our-to-our-leased-assign-field.dada +++ b/dada_tests/reservations/our-to-our-leased-assign-field.dada @@ -1,6 +1,6 @@ class Point(any a, any b) -class OurLeased(our leased f) +class OurLeased(shleased f) async fn main() { our p = Point(22, 44) # create a shared point `(22, 44)` diff --git a/dada_tests/reservations/our-to-our-leased-assign.dada b/dada_tests/reservations/our-to-our-leased-assign.dada index 8cc0b9c4..6f2a887e 100644 --- a/dada_tests/reservations/our-to-our-leased-assign.dada +++ b/dada_tests/reservations/our-to-our-leased-assign.dada @@ -5,7 +5,7 @@ async fn main() { # leasing an "our" thing becomes a second # owner (lessors are always exclusive) - our leased q = p + shleased q = p print(q).await #! OUTPUT Point\(22, 44\) # reassigning `p` does not invalidate `q`. diff --git a/dada_tests/reservations/our-to-our-leased-field.dada b/dada_tests/reservations/our-to-our-leased-field.dada index 216a5502..f312a757 100644 --- a/dada_tests/reservations/our-to-our-leased-field.dada +++ b/dada_tests/reservations/our-to-our-leased-field.dada @@ -1,6 +1,6 @@ class Point(any a, any b) -class OurLeased(our leased f) +class OurLeased(shleased f) async fn main() { our p = Point(22, 44) # create `(22, 44)` with shared ownership diff --git a/dada_tests/reservations/our-to-our-leased-var.dada b/dada_tests/reservations/our-to-our-leased-var.dada index 0a7da87b..32046f0e 100644 --- a/dada_tests/reservations/our-to-our-leased-var.dada +++ b/dada_tests/reservations/our-to-our-leased-var.dada @@ -2,7 +2,7 @@ class Point(any a, any b) async fn main() { our p = Point(22, 44) - our leased q = p # `q` becomes 2nd owner of `(22, 44)` + shleased q = p # `q` becomes 2nd owner of `(22, 44)` p := Point(44, 66) # reassigning `p` has no effect on `q` print(p).await #! OUTPUT Point\(44, 66\) diff --git a/dada_tests/specifier/leased-from-shared-rvalue-assign-in-loop.dada b/dada_tests/specifier/leased-from-shared-rvalue-assign-in-loop.dada index 7edc1b49..7d75f995 100644 --- a/dada_tests/specifier/leased-from-shared-rvalue-assign-in-loop.dada +++ b/dada_tests/specifier/leased-from-shared-rvalue-assign-in-loop.dada @@ -4,7 +4,7 @@ async fn main() { # Leasing an `our` value just takes ownership # of it, so `p` becomes (shared) owner of this # point here. - our leased p = Point(22, 44).share + shleased p = Point(22, 44).share i = 0 while i < 1 { diff --git a/dada_tests/specifier/need-any-got-our-leased.dada b/dada_tests/specifier/need-any-got-shleased.dada similarity index 100% rename from dada_tests/specifier/need-any-got-our-leased.dada rename to dada_tests/specifier/need-any-got-shleased.dada diff --git a/dada_tests/specifier/need-leased-got-our-leased/compiler-output.ref b/dada_tests/specifier/need-any-got-shleased/compiler-output.ref similarity index 100% rename from dada_tests/specifier/need-leased-got-our-leased/compiler-output.ref rename to dada_tests/specifier/need-any-got-shleased/compiler-output.ref diff --git a/dada_tests/specifier/need-any-got-our-leased/stdout.ref b/dada_tests/specifier/need-any-got-shleased/stdout.ref similarity index 100% rename from dada_tests/specifier/need-any-got-our-leased/stdout.ref rename to dada_tests/specifier/need-any-got-shleased/stdout.ref diff --git a/dada_tests/specifier/need-leased-got-our-leased.dada b/dada_tests/specifier/need-leased-got-shleased.dada similarity index 100% rename from dada_tests/specifier/need-leased-got-our-leased.dada rename to dada_tests/specifier/need-leased-got-shleased.dada diff --git a/dada_tests/specifier/need-my-got-our-leased/compiler-output.ref b/dada_tests/specifier/need-leased-got-shleased/compiler-output.ref similarity index 100% rename from dada_tests/specifier/need-my-got-our-leased/compiler-output.ref rename to dada_tests/specifier/need-leased-got-shleased/compiler-output.ref diff --git a/dada_tests/specifier/need-leased-got-our-leased/stdout.ref b/dada_tests/specifier/need-leased-got-shleased/stdout.ref similarity index 100% rename from dada_tests/specifier/need-leased-got-our-leased/stdout.ref rename to dada_tests/specifier/need-leased-got-shleased/stdout.ref diff --git a/dada_tests/specifier/need-my-got-our-leased.dada b/dada_tests/specifier/need-my-got-shleased.dada similarity index 100% rename from dada_tests/specifier/need-my-got-our-leased.dada rename to dada_tests/specifier/need-my-got-shleased.dada diff --git a/dada_tests/specifier/need-our-got-our-leased/compiler-output.ref b/dada_tests/specifier/need-my-got-shleased/compiler-output.ref similarity index 100% rename from dada_tests/specifier/need-our-got-our-leased/compiler-output.ref rename to dada_tests/specifier/need-my-got-shleased/compiler-output.ref diff --git a/dada_tests/specifier/need-my-got-our-leased/stdout.ref b/dada_tests/specifier/need-my-got-shleased/stdout.ref similarity index 100% rename from dada_tests/specifier/need-my-got-our-leased/stdout.ref rename to dada_tests/specifier/need-my-got-shleased/stdout.ref diff --git a/dada_tests/specifier/need-our-got-our-leased.dada b/dada_tests/specifier/need-our-got-shleased.dada similarity index 100% rename from dada_tests/specifier/need-our-got-our-leased.dada rename to dada_tests/specifier/need-our-got-shleased.dada diff --git a/dada_tests/specifier/need-our-leased-got-leased/compiler-output.ref b/dada_tests/specifier/need-our-got-shleased/compiler-output.ref similarity index 100% rename from dada_tests/specifier/need-our-leased-got-leased/compiler-output.ref rename to dada_tests/specifier/need-our-got-shleased/compiler-output.ref diff --git a/dada_tests/specifier/need-our-got-our-leased/stdout.ref b/dada_tests/specifier/need-our-got-shleased/stdout.ref similarity index 100% rename from dada_tests/specifier/need-our-got-our-leased/stdout.ref rename to dada_tests/specifier/need-our-got-shleased/stdout.ref diff --git a/dada_tests/specifier/need-our-leased-got-our-leased.dada b/dada_tests/specifier/need-our-leased-got-our-leased.dada deleted file mode 100644 index e5ca7ce6..00000000 --- a/dada_tests/specifier/need-our-leased-got-our-leased.dada +++ /dev/null @@ -1,5 +0,0 @@ -class Point() - -async fn main() { - our leased p = Point().lease.share -} \ No newline at end of file diff --git a/dada_tests/specifier/need-our-leased-got-our.dada b/dada_tests/specifier/need-shleased-got-leased.dada similarity index 50% rename from dada_tests/specifier/need-our-leased-got-our.dada rename to dada_tests/specifier/need-shleased-got-leased.dada index 758fff6a..6f5c35e8 100644 --- a/dada_tests/specifier/need-our-leased-got-our.dada +++ b/dada_tests/specifier/need-shleased-got-leased.dada @@ -1,5 +1,5 @@ class Point() async fn main() { - our leased p = Point().share + shleased p = Point().lease } \ No newline at end of file diff --git a/dada_tests/specifier/need-our-leased-got-my/compiler-output.ref b/dada_tests/specifier/need-shleased-got-leased/compiler-output.ref similarity index 100% rename from dada_tests/specifier/need-our-leased-got-my/compiler-output.ref rename to dada_tests/specifier/need-shleased-got-leased/compiler-output.ref diff --git a/dada_tests/specifier/need-our-leased-got-leased/stdout.ref b/dada_tests/specifier/need-shleased-got-leased/stdout.ref similarity index 100% rename from dada_tests/specifier/need-our-leased-got-leased/stdout.ref rename to dada_tests/specifier/need-shleased-got-leased/stdout.ref diff --git a/dada_tests/specifier/need-our-leased-got-my.dada b/dada_tests/specifier/need-shleased-got-my.dada similarity index 55% rename from dada_tests/specifier/need-our-leased-got-my.dada rename to dada_tests/specifier/need-shleased-got-my.dada index 59e86c11..50dcef59 100644 --- a/dada_tests/specifier/need-our-leased-got-my.dada +++ b/dada_tests/specifier/need-shleased-got-my.dada @@ -1,5 +1,5 @@ class Point() async fn main() { - our leased p = Point() + shleased p = Point() } \ No newline at end of file diff --git a/dada_tests/specifier/need-our-leased-got-our-leased/compiler-output.ref b/dada_tests/specifier/need-shleased-got-my/compiler-output.ref similarity index 100% rename from dada_tests/specifier/need-our-leased-got-our-leased/compiler-output.ref rename to dada_tests/specifier/need-shleased-got-my/compiler-output.ref diff --git a/dada_tests/specifier/need-our-leased-got-my/stdout.ref b/dada_tests/specifier/need-shleased-got-my/stdout.ref similarity index 100% rename from dada_tests/specifier/need-our-leased-got-my/stdout.ref rename to dada_tests/specifier/need-shleased-got-my/stdout.ref diff --git a/dada_tests/specifier/need-our-leased-got-leased.dada b/dada_tests/specifier/need-shleased-got-our.dada similarity index 50% rename from dada_tests/specifier/need-our-leased-got-leased.dada rename to dada_tests/specifier/need-shleased-got-our.dada index 189b450e..5bc1dd3c 100644 --- a/dada_tests/specifier/need-our-leased-got-leased.dada +++ b/dada_tests/specifier/need-shleased-got-our.dada @@ -1,5 +1,5 @@ class Point() async fn main() { - our leased p = Point().lease + shleased p = Point().share } \ No newline at end of file diff --git a/dada_tests/specifier/our-leased-from-shared-rvalue-assign-in-loop/compiler-output.ref b/dada_tests/specifier/need-shleased-got-our/compiler-output.ref similarity index 100% rename from dada_tests/specifier/our-leased-from-shared-rvalue-assign-in-loop/compiler-output.ref rename to dada_tests/specifier/need-shleased-got-our/compiler-output.ref diff --git a/dada_tests/specifier/need-our-leased-got-our-leased/stdout.ref b/dada_tests/specifier/need-shleased-got-our/stdout.ref similarity index 100% rename from dada_tests/specifier/need-our-leased-got-our-leased/stdout.ref rename to dada_tests/specifier/need-shleased-got-our/stdout.ref diff --git a/dada_tests/specifier/need-shleased-got-shleased.dada b/dada_tests/specifier/need-shleased-got-shleased.dada new file mode 100644 index 00000000..70a00da9 --- /dev/null +++ b/dada_tests/specifier/need-shleased-got-shleased.dada @@ -0,0 +1,5 @@ +class Point() + +async fn main() { + shleased p = Point().lease.share +} \ No newline at end of file diff --git a/dada_tests/specifier/our-leased-got-my-then-copy/compiler-output.ref b/dada_tests/specifier/need-shleased-got-shleased/compiler-output.ref similarity index 100% rename from dada_tests/specifier/our-leased-got-my-then-copy/compiler-output.ref rename to dada_tests/specifier/need-shleased-got-shleased/compiler-output.ref diff --git a/dada_tests/specifier/need-shleased-got-shleased/stdout.ref b/dada_tests/specifier/need-shleased-got-shleased/stdout.ref new file mode 100644 index 00000000..e69de29b diff --git a/dada_tests/specifier/our-lease-does-not-yield-leased.dada b/dada_tests/specifier/our-lease-does-not-yield-leased.dada new file mode 100644 index 00000000..020164df --- /dev/null +++ b/dada_tests/specifier/our-lease-does-not-yield-leased.dada @@ -0,0 +1,9 @@ +class Point(our x, our y) + +async fn main() { + our p = Point(22, 33) + + # Leasing an `our` does not yield a `leased` value + # (`leased` implies unique access). + leased x = p.x.lease #! RUN ERROR more permissions needed +} diff --git a/dada_tests/specifier/our-lease-does-not-yield-leased/compiler-output.ref b/dada_tests/specifier/our-lease-does-not-yield-leased/compiler-output.ref new file mode 100644 index 00000000..e69de29b diff --git a/dada_tests/specifier/our-lease-does-not-yield-leased/stdout.ref b/dada_tests/specifier/our-lease-does-not-yield-leased/stdout.ref new file mode 100644 index 00000000..e69de29b diff --git a/dada_tests/specifier/our-lease-yields-our.dada b/dada_tests/specifier/our-lease-yields-our.dada new file mode 100644 index 00000000..867fb86c --- /dev/null +++ b/dada_tests/specifier/our-lease-yields-our.dada @@ -0,0 +1,10 @@ +class Point(our x, our y) + +async fn main() { + our p = Point(22, 33) + + # Under current semantics, leasing an `our` + # yields another `our` value (not, e.g., shleased), + # so this code works. + our x = p.x.lease +} diff --git a/dada_tests/specifier/our-lease-yields-our/compiler-output.ref b/dada_tests/specifier/our-lease-yields-our/compiler-output.ref new file mode 100644 index 00000000..e69de29b diff --git a/dada_tests/specifier/our-lease-yields-our/stdout.ref b/dada_tests/specifier/our-lease-yields-our/stdout.ref new file mode 100644 index 00000000..e69de29b diff --git a/dada_tests/specifier/our-leased-got-my-then-copy.dada b/dada_tests/specifier/our-leased-got-my-then-copy.dada deleted file mode 100644 index 2b69071a..00000000 --- a/dada_tests/specifier/our-leased-got-my-then-copy.dada +++ /dev/null @@ -1,7 +0,0 @@ -class Point(our x, our y) - -async fn main() { - p = Point(22, 33) - q = p - print(p).await #! OUTPUT Point\(22, 33\) -} diff --git a/dada_tests/specifier/our-leased-got-my-then-copy/stdout.ref b/dada_tests/specifier/our-leased-got-my-then-copy/stdout.ref deleted file mode 100644 index dce04907..00000000 --- a/dada_tests/specifier/our-leased-got-my-then-copy/stdout.ref +++ /dev/null @@ -1 +0,0 @@ -our leased Point(22, 33) diff --git a/dada_tests/specifier/our-shlease-yields-our.dada b/dada_tests/specifier/our-shlease-yields-our.dada new file mode 100644 index 00000000..0ce59afd --- /dev/null +++ b/dada_tests/specifier/our-shlease-yields-our.dada @@ -0,0 +1,10 @@ +class Point(our x, our y) + +async fn main() { + our p = Point(22, 33) + + # Under current semantics, shleasing an `our` + # yields another `our` value (not, e.g., shleased), + # so this code works. + our x = p.x.shlease +} diff --git a/dada_tests/specifier/our-shlease-yields-our/compiler-output.ref b/dada_tests/specifier/our-shlease-yields-our/compiler-output.ref new file mode 100644 index 00000000..e69de29b diff --git a/dada_tests/specifier/our-shlease-yields-our/stdout.ref b/dada_tests/specifier/our-shlease-yields-our/stdout.ref new file mode 100644 index 00000000..e69de29b diff --git a/dada_tests/specifier/our-leased-from-shared-rvalue-assign-in-loop.dada b/dada_tests/specifier/shleased-from-shared-rvalue-assign-in-loop.dada similarity index 93% rename from dada_tests/specifier/our-leased-from-shared-rvalue-assign-in-loop.dada rename to dada_tests/specifier/shleased-from-shared-rvalue-assign-in-loop.dada index 7edc1b49..7d75f995 100644 --- a/dada_tests/specifier/our-leased-from-shared-rvalue-assign-in-loop.dada +++ b/dada_tests/specifier/shleased-from-shared-rvalue-assign-in-loop.dada @@ -4,7 +4,7 @@ async fn main() { # Leasing an `our` value just takes ownership # of it, so `p` becomes (shared) owner of this # point here. - our leased p = Point(22, 44).share + shleased p = Point(22, 44).share i = 0 while i < 1 { diff --git a/dada_tests/specifier/shleased-from-shared-rvalue-assign-in-loop/compiler-output.ref b/dada_tests/specifier/shleased-from-shared-rvalue-assign-in-loop/compiler-output.ref new file mode 100644 index 00000000..e69de29b diff --git a/dada_tests/specifier/our-leased-from-shared-rvalue-assign-in-loop/stdout.ref b/dada_tests/specifier/shleased-from-shared-rvalue-assign-in-loop/stdout.ref similarity index 100% rename from dada_tests/specifier/our-leased-from-shared-rvalue-assign-in-loop/stdout.ref rename to dada_tests/specifier/shleased-from-shared-rvalue-assign-in-loop/stdout.ref diff --git a/dada_tests/specifier/shleased-got-my-then-copy.dada b/dada_tests/specifier/shleased-got-my-then-copy.dada new file mode 100644 index 00000000..b57af6ed --- /dev/null +++ b/dada_tests/specifier/shleased-got-my-then-copy.dada @@ -0,0 +1,12 @@ +class Point(our x, our y) + +async fn main() { + # `p` is shleased here from a temporary; scope of the temporary is the block + p = Point(22, 33) + + # ...and then we copy it to `q` (also shleased) + q = p + + # ...and check if we can access `p` + print(p).await #! OUTPUT Point\(22, 33\) +} diff --git a/dada_tests/specifier/shleased-got-my-then-copy/compiler-output.ref b/dada_tests/specifier/shleased-got-my-then-copy/compiler-output.ref new file mode 100644 index 00000000..e69de29b diff --git a/dada_tests/specifier/shleased-got-my-then-copy/stdout.ref b/dada_tests/specifier/shleased-got-my-then-copy/stdout.ref new file mode 100644 index 00000000..463a12ff --- /dev/null +++ b/dada_tests/specifier/shleased-got-my-then-copy/stdout.ref @@ -0,0 +1 @@ +shleased Point(22, 33) diff --git a/dada_tests/validate/op-eq/lhs_shared_field_of_func_call.dada b/dada_tests/validate/op-eq/lhs_shared_field_of_func_call.dada index 0b544471..9099324c 100644 --- a/dada_tests/validate/op-eq/lhs_shared_field_of_func_call.dada +++ b/dada_tests/validate/op-eq/lhs_shared_field_of_func_call.dada @@ -8,7 +8,7 @@ async fn main() { print(p).await } -async fn test(our leased p) { +async fn test(shleased p) { print("Hi").await #! OUTPUT Hi p } \ No newline at end of file