Liveness and cancellation

In the previous sub-chapters, we saw how permissions are compared structurally – place ordering and the copy permission hierarchy. But those rules assume all borrowed places are still alive.

What happens when a borrowed place is dead – no longer used by later code?

Dead links in a RedChain can be cancelled or promoted, which enables subtyping relationships that wouldn’t hold for live links. This is Dada’s equivalent of Rust’s non-lexical lifetimes (NLL) – borrows end when the reference is last used, not when it goes out of scope.

A motivating example: re-borrowing

Consider a function that re-borrows a lease:

crate::assert_ok!(
    {
        class Data { }

        class Main {
            fn test(given self) {
                let d = new Data();
                let p: mut[d] Data = d.mut;
                let q: mut[p] Data = p.mut;
                let r: mut[d] Data = q.give;
                ();
            }
        }
    }
);

Here’s what happens step by step:

1. d is created with type given Data
2. p: mut[d] Data – a mutable lease of d
3. q: mut[p] Data – a mutable lease of p (a re-borrow)
4. r: mut[d] Data – we want q.give to have type mut[d] Data

The expression q.give has type mut[p] Data. But r expects mut[d] Data. How can mut[p] mut[d] become mut[d]?

When we reduce mut[p], the permission for q.give, we get the chain [Mtd(p)] – p is dead because q.give is the last expression, and p is never used again. Chain expansion follows p’s type (mut[d] Data), appending Mtl(d) to get [Mtd(p), Mtl(d)].

The target mut[d] reduces to [Mtl(d)].

Comparing [Mtd(p), Mtl(d)] vs [Mtl(d)]: the cancellation rule fires – since p is dead, the Mtd(p) link is dropped, and comparison continues with the tail [Mtl(d)] vs [Mtl(d)], which succeeds.

But not when the place is live

If p is still used after the assignment, cancellation is blocked:

crate::assert_err!(
    {
        class Data {
            fn read[perm P](P self) { (); }
        }

        class Main {
            fn test(given self) {
                let d = new Data();
                let p: mut[d] Data = d.mut;
                let q: mut[p] Data = p.mut;
                let r: mut[d] Data = q.give;
                p.give.read[mut[d]]();
            }
        }
    },
    expect_test::expect![[r#"
        the rule "(mut::P) vs (mut::P)" at (redperms.rs) failed because
          condition evaluted to false: `place_b.is_prefix_of(place_a)`
            place_b = d
            place_a = p"#]]
);

Here p appears in p.give.read[...]() after q.give, so p is live at the point where q.give is evaluated. The chain becomes [Mtl(p), Mtl(d)] (live, not dead) – and there is no rule to cancel a live Mtl link. The assignment to r: mut[d] Data fails.

The two cancellation operations

Dead links are resolved by two rules in red_chain_sub_chain:

Cancellation: dropping a dead mut link

(let ty_dead = env.place_ty(place_dead)?)
(prove_is_shareable(env, ty_dead) => ())
(prove_is_mut(env, tail_a) => ())
(red_chain_sub_chain(env, tail_a, red_chain_b) => ())
--- ("(mut-dead::P) vs Q ~~> (P) vs Q")
(red_chain_sub_chain(env, Head(RedLink::Mtd(place_dead), Tail(tail_a)), red_chain_b) => ())

When the chain starts with Mtd(place) (a dead mutable lease), the rule drops it and continues comparing the tail against the target.

Three conditions must hold:

1. The place must be dead (encoded by the Mtd variant)
2. The type of the dead place must be shareable – prove_is_shareable(env.place_ty(place_dead))
3. The tail must be mut-based – prove_is_mut(tail_a)

The shareable check ensures it’s safe to silently release the lease. The tail check ensures we’re cancelling a lien on top of another lease, not an owned permission.

Promotion: converting a dead ref to shared

(let ty_dead = env.place_ty(place_dead)?)
(prove_is_shareable(env, ty_dead) => ())
(prove_is_mut(env, tail_a) => ())
(red_chain_sub_chain(env, Head(RedLink::Shared, Tail(tail_a)), red_chain_b) => ())
--- ("(ref-dead::P) vs Q ~~> (shared::P) vs Q")
(red_chain_sub_chain(env, Head(RedLink::Rfd(place_dead), Tail(tail_a)), red_chain_b) => ())

When the chain starts with Rfd(place) (a dead reference), the rule replaces it with Shared and continues comparing.

This reflects the fact that once the borrowed place is dead, the reference effectively becomes shared – no one can invalidate it through the original place anymore.

Here’s an example of promotion in action:

crate::assert_ok!(
    {
        class Data { }

        class Main {
            fn test(given self) {
                let d = new Data();
                let p: mut[d] Data = d.mut;
                let q: ref[p] Data = p.ref;
                let r: shared mut[d] Data = q.give;
                ();
            }
        }
    }
);

The expression q.give has type ref[p] mut[d] Data. The target r expects shared mut[d] Data. Since p is dead, the chain [Rfd(p), Mtl(d)] promotes Rfd(p) to Shared, giving [Shared, Mtl(d)] which matches shared mut[d].

If p were still live, promotion wouldn’t happen:

crate::assert_err!(
    {
        class Data {
            fn read[perm P](P self) { (); }
        }

        class Main {
            fn test(given self) {
                let d = new Data();
                let p: mut[d] Data = d.mut;
                let q: ref[p] Data = p.ref;
                let r: shared mut[d] Data = q.give;
                p.give.read[mut[d]]();
            }
        }
    },
    expect_test::expect![[r#"
        the rule "(ref::P) vs (shared::mut::P)" at (redperms.rs) failed because
          condition evaluted to false: `place_b.is_prefix_of(place_a)`
            place_b = d
            place_a = p"#]]
);

With p live, the chain is [Rfl(p), Mtl(d)] – the Rfl variant has no promotion rule, and the comparison fails.

A practical pattern: re-borrowing in functions

Liveness-based cancellation enables a common pattern – re-borrowing inside a function and returning the result:

crate::assert_ok!(
    {
        class Data { }

        class Main {
            fn reborrow(given self, d: mut[self] Data) -> mut[self] Data {
                let p: mut[d] Data = d.mut;
                p.give;
            }
        }
    }
);

The parameter d: mut[self] Data is a mutable lease from self. Inside the function, d.mut creates mut[d] Data – a re-borrow. When we return p.give, its type is mut[d] Data. The return type expects mut[self] Data.

Since d is dead at the return point (it’s a parameter that’s not used after p.give), the Mtd(d) link cancels, and the chain collapses to mut[self].

Without liveness-based cancellation, re-borrowing would be useless – you could never return a value that was transiently borrowed through a local.

What cancellation cannot do

Not all dead links can be resolved. There are important limits on when cancellation and promotion apply.

Shared-to-leased conversion is blocked

Cancellation can resolve links within a permission chain, but it cannot change the nature of a permission from shared (copy) to leased (exclusive):

crate::assert_err!(
    {
        class Data { }

        class Main {
            fn test(given self) {
                let d = new Data();
                let p: mut[d] Data = d.mut;
                let q: ref[p] mut[d] Data = p.ref;
                let r: mut[d] Data = q.give;
                ();
            }
        }
    },
    expect_test::expect!["judgment had no applicable rules: `check_program { program: class Data { } class Main { fn test (given self) -> () { let d = new Data () ; let p : mut [d] Data = d . mut ; let q : ref [p] mut [d] Data = p . ref ; let r : mut [d] Data = q . give ; () ; } } }`"]
);

The expression q.give has type ref[p] mut[d] Data. Even though p is dead, the chain [Rfd(p), Mtl(d)] cannot become [Mtl(d)].

Why? Promotion converts Rfd(p) to Shared, giving [Shared, Mtl(d)] – a shared lease. But mut[d] reduces to [Mtl(d)] – an exclusive lease. shared mut[d] is not a subtype of mut[d].

This reflects a real safety invariant: a reference (even a dead one) was shared – multiple copies may exist. You can’t recover exclusive access from something that was shared.

Multi-place permissions: all places must be dead

When a permission mentions multiple places, like ref[p, q], reduction produces one chain per place. For cancellation to resolve all of them, every place must be dead:

crate::assert_ok!(
    {
        class Data { }

        class Main {
            fn test(given self) {
                let d = new Data();
                let p: ref[d] Data = d.ref;
                let q: ref[d] Data = d.ref;
                let r: ref[p, q] ref[d] Data = p.ref;
                let s: ref[d] Data = r.give;
                ();
            }
        }
    }
);

Both p and q are dead at the point of r.give, so both Rfd(p) and Rfd(q) chains can be resolved.

But if even one place is still live:

crate::assert_err!(
    {
        class Data { }

        class Main {
            fn test(given self) {
                let d = new Data();
                let p: ref[d] Data = d.ref;
                let q: ref[d] Data = d.ref;
                let r: ref[p, q] ref[d] Data = p.ref;
                let s: ref[d] Data = r.give;
                q.give;
            }
        }
    },
    expect_test::expect!["judgment had no applicable rules: `check_program { program: class Data { } class Main { fn test (given self) -> () { let d = new Data () ; let p : ref [d] Data = d . ref ; let q : ref [d] Data = d . ref ; let r : ref [p, q] ref [d] Data = p . ref ; let s : ref [d] Data = r . give ; q . give ; } } }`"]
);

Here q is used after r.give (in q.give), so q is live at the point where r.give is evaluated. The chain Rfl(q) (live, not dead) has no cancellation rule, and the comparison fails – even though p is dead and its chain could be resolved.

How liveness is computed

Liveness is computed backwards through the program. Starting from the end of the function body (where nothing is live), the analysis walks statements in reverse, tracking which places are accessed or traversed.

A place is live if:

• It or any overlapping place is accessed later, or
• It is a prefix of a place that gets assigned to later

A place is dead if it is not live – no future code reads from it or any of its sub-places.

This backward analysis means liveness depends on what comes after a given point in the program. The same variable can be live at one point and dead at another.

The type system threads LivePlaces through the checking process: when sub_perms is called, it receives the set of places that are live after the current expression. This is what determines whether a ref[d] or mut[d] reduces to the live variant (Rfl/Mtl) or the dead variant (Rfd/Mtd).

Summary

Key constraints:

• Only dead links can be cancelled or promoted
• The dead place’s type must be shareable
• The tail of the chain must be mut-based
• Shared-to-leased conversion is never possible
• Multi-place permissions require all places to be dead
• Liveness is computed backwards from end of function