Sharing

In the previous chapter, we saw that giving a non-copyable value moves it – after a give, the original is gone. We also saw that shared class types like Int are copyable and can be given multiple times. But what about regular classes? What if you want to use a value in multiple places without giving up ownership?

That’s what sharing is for.

Sharing a value

The .share operator converts a value from unique (given) ownership to shared ownership. Once shared, a value can be freely copied:

crate::assert_ok!(
    {
        class Data { }

        class Main {
            fn test(given self) -> shared Data {
                let d = new Data();
                let s = d.give.share;
                s.give;
                s.give;
            }
        }
    }
);

Compare this with the giving a value twice example from the previous chapter, which failed. The difference is .share – it transforms the Data value so that subsequent gives copy rather than move.

The share expr rule

The type checker handles .share with this rule:

(type_expr(env, live_after, &**expr) => (env, ty))
(prove_is_shareable(env, ty) => ())
----------------------------------- ("share expr")
(type_expr(env, live_after, Expr::Share(expr)) => (env, Ty::apply_perm(Perm::Shared, ty)))

The rule has two premises:

• type_expr(env, ..., &*expr) => (env, ty) – Type-check the inner expression, producing a type ty.

• prove_is_shareable(&env, &ty) => () – Verify that the type is allowed to be shared. Not all types can be shared – given classes cannot.

If both premises succeed, the result type is shared ty – the original type wrapped with the shared permission.

Shareability and class predicates

Whether a type can be shared depends on its class predicate. Classes come in three flavors:

#[term]
#[derive(Copy, Default)]
pub enum ClassPredicate {
    /// `Given` classes are permitted to have destructors (FIXME: we don't model those right now).
    /// A `Given` class cannot be shared and, since they have a destructor, we cannot drop them
    /// from borrow chains (i.e., `mut[guard] mut[data]` cannot be converted to `mut[data]`
    /// even if `guard` is not live since, in fact, the variable *will* be used again by the dtor).
    #[grammar(given)]
    Given,

    /// `Share` classes are the default. They indicate classes that, while unique by default,
    /// can be shared with `.give.share` to create a `shared Class` that is copyable around.
    #[default]
    Share,

    /// `Shared` classes are value types that are always considered shared
    /// and hence can be copied freely. However, their fields
    /// cannot be individually mutated as a result.
    #[grammar(shared)]
    Shared,
}

The prove_is_shareable judgment delegates to the general predicate-proving machinery:

(prove_predicate(env, Predicate::share(a)) => ())
---------------------------- ("is")
(prove_is_shareable(env, a) => ())

For a regular class like Data, the Share predicate is satisfied by default, so .share succeeds.

Shared values are copyable

Once a value is shared, the move_place judgment from the giving chapter treats it differently. Recall that move_place has two rules – “give” (move) and “copy”. The “copy” rule requires prove_is_copy:

(if live_after.is_live(place))!
(prove_is_copy(env, ty) => ())
----------------------------------- ("copy")
(move_place(env, _live_after, _place, ty) => env)

A shared Data type satisfies prove_is_copy because the shared permission is a copy permission. So when you write s.give on a shared value, the “copy” rule fires and the value is copied rather than moved.

This is why the example above works – both s.give expressions copy the shared value.

Shared classes are always shared

In the previous chapter, we saw that Int values can be given multiple times. That’s because Int is a shared class type – it has the Shared class predicate, which means it is always shared and copyable without needing an explicit .share:

crate::assert_ok!(
    {
        shared class Point {
            x: Int;
            y: Int;
        }

        class Main {
            fn test(given self) -> Point {
                let p = new Point(22, 44);
                p.give;
                p.give;
            }
        }
    }
);

Shared classes are always copyable, but their fields cannot be individually mutated. Regular classes are mutable by default but require .share to become copyable.

Given classes cannot be shared

Given classes cannot be shared. Attempting to share a given class is an error:

crate::assert_err!(
    {
        given class Resource { }

        class Main {
            fn test(given self) -> shared Resource {
                let r = new Resource();
                r.give.share;
            }
        }
    },
    expect_test::expect![[r#"
        the rule "share class" at (predicates.rs) failed because
          pattern `true` did not match value `false`"#]]
);

The prove_is_shareable premise fails because Resource has the Given predicate, which does not satisfy share(Resource).

Sharing is idempotent

Sharing an already-shared value is fine – it’s a no-op:

crate::assert_ok!(
    {
        class Data { }

        class Main {
            fn test(given self) -> shared Data {
                let d = new Data();
                d.give.share.share;
            }
        }
    }
);

The inner .share produces shared Data. The outer .share checks prove_is_shareable on shared Data, which succeeds because a shared permission is always shareable. The result is still shared Data – applying shared to an already-shared type normalizes to the same type.