-
Notifications
You must be signed in to change notification settings - Fork 1.9k
"borrow checker invariants" section of the "leveraging the type system" chapter #2867
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Open
tall-vase
wants to merge
15
commits into
google:main
Choose a base branch
from
tall-vase:idiomatic/typesystem-borrowchecker
base: main
Could not load branches
Branch not found: {{ refName }}
Loading
Could not load tags
Nothing to show
Loading
Are you sure you want to change the base?
Some commits from the old base branch may be removed from the timeline,
and old review comments may become outdated.
+406
−0
Open
Changes from all commits
Commits
Show all changes
15 commits
Select commit
Hold shift + click to select a range
b771e7f
Initial draft of the 'borrow checker invariants' section
tall-vase 3831858
Elaborate more on the cryptography example
tall-vase a81b55a
Begin expanding the slide notes, rename the external resources sectio…
tall-vase 0b4318f
Get this section into a 'review ready' state.
tall-vase 728af30
Reset all minutes on the borrowck invariants section to 0
tall-vase a37a272
General editing pass based off feedback
tall-vase 88852f2
Minor editing
tall-vase 0aa4f21
Another editing pass
tall-vase 37e69fe
minor grammar edit
tall-vase 595ca8e
Another editing pass
tall-vase 2a88748
Formatting pass
31284d6
Merge branch 'main' into idiomatic/typesystem-borrowchecker
tall-vase e7f874b
fix test errors, make sure compilation succeeds after erroneous lines…
808de4f
Address lints
85b70f0
Address lints
File filter
Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
There are no files selected for viewing
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
80 changes: 80 additions & 0 deletions
80
src/idiomatic/leveraging-the-type-system/borrow-checker-invariants.md
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,80 @@ | ||
--- | ||
minutes: 0 | ||
--- | ||
|
||
# Using the Borrow checker to enforce Invariants | ||
|
||
The logic of the borrow checker, while tied to "memory ownership", can be | ||
abstracted away from this central use case to model other problems and prevent | ||
API misuse. | ||
|
||
```rust,editable | ||
fn main() { | ||
// Doors can be open or closed, and you need the right key to lock or unlock | ||
// one. Modelled with a Shared key and Owned door. | ||
pub struct DoorKey { | ||
pub key_shape: u32, | ||
} | ||
pub struct LockedDoor { | ||
lock_shape: u32, | ||
} | ||
pub struct OpenDoor { | ||
lock_shape: u32, | ||
} | ||
|
||
fn open_door(key: &DoorKey, door: LockedDoor) -> Result<OpenDoor, LockedDoor> { | ||
if door.lock_shape == key.key_shape { | ||
Ok(OpenDoor { lock_shape: door.lock_shape }) | ||
} else { | ||
Err(door) | ||
} | ||
} | ||
|
||
fn close_door(key: &DoorKey, door: OpenDoor) -> Result<LockedDoor, OpenDoor> { | ||
if door.lock_shape == key.key_shape { | ||
Ok(LockedDoor { lock_shape: door.lock_shape }) | ||
} else { | ||
Err(door) | ||
} | ||
} | ||
|
||
let key = DoorKey { key_shape: 7 }; | ||
let closed_door = LockedDoor { lock_shape: 7 }; | ||
let opened_door = open_door(&key, closed_door); | ||
if let Ok(opened_door) = opened_door { | ||
println!("Opened the door with key shape '{}'", key.key_shape); | ||
} else { | ||
eprintln!( | ||
"Door wasn't opened! Your key only opens locks with shape '{}'", | ||
key.key_shape | ||
); | ||
} | ||
} | ||
``` | ||
|
||
<details> | ||
|
||
<!-- TODO: link to typestate when that gets merged. --> | ||
|
||
- The borrow checker has been used to prevent use-after-free and multiple | ||
mutable references up until this point, and we've used types to shape and | ||
restrict use of APIs already using the "typestate" pattern. | ||
|
||
- This example uses the ownership & borrowing rules to model the locking and | ||
unlocking of a door. We can try to open a door with a key, but if it's the | ||
wrong key the door is still closed (here represented as an error) and the key | ||
persists regardless. | ||
|
||
- The rules of the borrow checker exist to prevent developers from accessing, | ||
changing, and holding onto data in memory in unpredictable ways without being | ||
so restrictive that it would prevent _writing software_. The underlying | ||
logical system does not "know" what memory is. All it does is enforce a | ||
specific set of rules of how different operations affect what later operations | ||
are possible. | ||
|
||
- Those rules can apply to many other cases: We can piggy-back onto the rules of | ||
the borrow checker to design APIs to be harder or impossible to misuse, even | ||
when there's little or no "memory safety" concerns in the problem domain. This | ||
section will walk through some of those different domains. | ||
|
||
</details> |
89 changes: 89 additions & 0 deletions
89
...leveraging-the-type-system/borrow-checker-invariants/aliasing-xor-mutability.md
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,89 @@ | ||
--- | ||
minutes: 0 | ||
--- | ||
|
||
# Mutually Exclusive References, or "Aliasing XOR Mutability" | ||
|
||
We can use the mutual exclusion of `&T` and `&mut T` references for a single | ||
value to model some constraints. | ||
|
||
```rust,editable,compile_fail | ||
pub struct Transaction(/* some kind of interior state */); | ||
pub struct QueryResult(String); | ||
|
||
pub struct DatabaseConnection { | ||
transaction: Transaction, | ||
query_results: Vec<QueryResult>, | ||
} | ||
|
||
impl DatabaseConnection { | ||
pub fn new() -> Self { | ||
Self { | ||
transaction: Transaction(/* again, pretend there's some interior state */), | ||
query_results: vec![], | ||
} | ||
} | ||
pub fn get_transaction(&mut self) -> &mut Transaction { | ||
&mut self.transaction | ||
} | ||
pub fn results(&self) -> &[QueryResult] { | ||
&self.query_results | ||
} | ||
pub fn commit(&mut self) { | ||
println!("Transaction committed!") | ||
} | ||
} | ||
|
||
pub fn do_something_with_transaction(transaction: &mut Transaction) {} | ||
|
||
fn main() { | ||
let mut db = DatabaseConnection::new(); | ||
let mut transaction = db.get_transaction(); | ||
do_something_with_transaction(transaction); | ||
let assumed_the_transactions_happened_immediately = db.results(); // ❌🔨 | ||
do_something_with_transaction(transaction); | ||
// Works, as the lifetime of "transaction" as a reference ended above. | ||
let assumed_the_transactions_happened_immediately_again = db.results(); | ||
db.commit(); | ||
} | ||
``` | ||
|
||
<details> | ||
|
||
- Aliasing XOR Mutability means "we can have multiple immutable references, a | ||
single mutable reference, but not both." | ||
|
||
- This example shows how we can use the mutual exclusion of these kinds of | ||
references to dissuade a user from reading query results while using a | ||
transaction API, something that might happen if the user is working under the | ||
false assumption that the queries being written to the transaction happen | ||
"immediately" rather than being queued up and performed together. | ||
|
||
- By borrowing one field of a struct under a mutable / exclusive reference we | ||
prevent access to the other fields of that struct under a shared / | ||
non-exclusive reference until the lifetime of that borrow ends. | ||
|
||
- As laid out in [generalizing ownership](generalizing-ownership.md) we can look | ||
at the ways Mutable References and Shareable References interact to see if | ||
they fit with the invariants we want to uphold for an API. | ||
|
||
- In this case, having the query results not public and placed behind a getter | ||
function, we can enforce the invariant "users of this API are not looking at | ||
the query results at the same time as they are writing to a transaction." | ||
|
||
<!-- Setup for Exercises --> | ||
<details> | ||
<summary> | ||
The "don't look at query results while building a transaction" invariant can still be circumvented, how so? | ||
</summary> | ||
<ul> | ||
<li> | ||
The user could access the transaction solely through `db.get_transaction()`, leaving the lifetime too temporary to prevent access to `db.results()`. | ||
</li> | ||
<li> | ||
How could we avoid this by working in other concepts from "Leveraging the Type System"? | ||
</li> | ||
</ul> | ||
</details> | ||
|
||
</details> |
69 changes: 69 additions & 0 deletions
69
.../leveraging-the-type-system/borrow-checker-invariants/generalizing-ownership.md
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,69 @@ | ||
--- | ||
minutes: 0 | ||
--- | ||
|
||
# Generalizing Ownership | ||
|
||
The logic of the borrow checker, while modelled off "memory ownership", can be | ||
abstracted away from that use case to model other problems where we want to | ||
prevent API misuse. | ||
|
||
```rust,editable,compile_fail | ||
// An internal data type to have something to hold onto. | ||
pub struct Internal; | ||
// The "outer" data. | ||
pub struct Data(Internal); | ||
|
||
fn shared_use(value: &Data) -> &Internal { | ||
&value.0 | ||
} | ||
fn exclusive_use(value: &mut Data) -> &mut Internal { | ||
&mut value.0 | ||
} | ||
fn deny_future_use(value: Data) {} | ||
|
||
fn main() { | ||
let mut value = Data(Internal); | ||
let deny_mut = shared_use(&value); | ||
let try_to_deny_immutable = exclusive_use(&mut value); // ❌🔨 | ||
let more_mut_denial = &deny_mut; | ||
deny_future_use(value); | ||
let even_more_mut_denial = shared_use(&value); // ❌🔨 | ||
} | ||
``` | ||
|
||
<details> | ||
|
||
- This example re-frames the borrow checker rules away from references and | ||
towards semantic meaning in non-memory-safety settings. Nothing is being | ||
mutated, nothing is being sent across threads. | ||
|
||
- To use the borrow checker as a problem solving tool, we will need to "forget" | ||
that the original purpose of it is to prevent mutable aliasing in the context | ||
of concurrency & dangling pointers, instead imagining and working within | ||
situations where the rules are the same but the meaning is slightly different. | ||
|
||
- In rust's borrow checker we have access to three different ways of "taking" a | ||
value: | ||
|
||
<!-- TODO: actually link to the RAII section when it has been merged. --> | ||
- Owned value `T`. Very permissive case, to the point where mutability can be | ||
re-set, but demands that nothing else is using it in any context and drops | ||
the value when scope ends (unless that scope returns this value) (see: | ||
RAII.) | ||
|
||
- Mutable Reference `&mut T`. While holding onto a mutable reference we can | ||
still "dispatch" to methods and functions that take an immutable, shared | ||
reference of the value but only as long as we're not aliasing immutable, | ||
shared references to related data "after" that dispatch. | ||
|
||
- Shared Reference `&T`. Allows aliasing but prevents mutable access while any | ||
of these exist. We can't "dispatch" to methods and functions that take | ||
mutable references when all we have is a shared reference. | ||
|
||
- Remember that every `&T` and `&mut T` has an _implicit lifetime._ We get to | ||
avoid annotating a lot of lifetimes because the rust compiler can infer the | ||
majority of them. See: | ||
[Lifetime Elision](../../../lifetimes/lifetime-elision.md). | ||
|
||
</details> |
101 changes: 101 additions & 0 deletions
101
...ic/leveraging-the-type-system/borrow-checker-invariants/lifetime-connections.md
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,101 @@ | ||
--- | ||
minutes: 0 | ||
--- | ||
|
||
# Lifetime "Connections" & External Resources | ||
|
||
Using `PhantomData` in conjunction with lifetimes lets us say "this value may | ||
own its data, but it can only live as long as the value that generated it" in | ||
rust's type system. | ||
|
||
```rust,editable,compile_fail | ||
fn main() { | ||
use std::marker::PhantomData; | ||
pub struct Tag; | ||
pub struct ErasedData<'a> { | ||
data: String, | ||
_phantom: PhantomData<&'a ()>, | ||
} | ||
impl<'a> ErasedData<'a> { | ||
pub fn get(&self) -> &str { | ||
&self.data | ||
} | ||
} | ||
pub struct TaggedData<T> { | ||
data: String, | ||
_phantom: PhantomData<T>, | ||
} | ||
tall-vase marked this conversation as resolved.
Show resolved
Hide resolved
|
||
impl<T> TaggedData<T> { | ||
pub fn new(data: String) -> Self { | ||
Self { data, _phantom: PhantomData } | ||
} | ||
pub fn consume(self) {} | ||
pub fn get_erased(&self) -> ErasedData<'_> { | ||
// has an owned String, but _phantom holds onto the lifetime of the | ||
// TaggedData that created it. | ||
ErasedData { data: self.data.clone(), _phantom: PhantomData } | ||
} | ||
} | ||
|
||
let tagged_data: TaggedData<Tag> = TaggedData::new("Real Data".to_owned()); | ||
// Get the erased-but-still-linked data. | ||
let erased_owned_and_linked = tagged_data.get_erased(); | ||
tagged_data.consume(); | ||
// Owned by `erased_owned_and_linked` but still connected to `tagged_data`. | ||
println!("{}", erased_owned_and_linked.get()); // ❌🔨 | ||
} | ||
``` | ||
|
||
<details> | ||
|
||
- `PhantomData` lets developers "tag" types with type and lifetime parameters | ||
that are not "really" present in the struct or enum. | ||
|
||
`PhantomData` can be used with the Typestate pattern to have data with the | ||
same structure i.e. `TaggedData<Start>` can have methods or trait | ||
implementations that `TaggedData<End>` doesn't. | ||
|
||
It can also be used to encode a connection between the lifetime of one value | ||
and another, while both values still maintain separate owned data within them. | ||
|
||
- This is really useful for modelling a bunch of relationships between data, | ||
where we want to establish that while a type has owned values within it is | ||
still connected to another piece of data and can only live as long as it. | ||
|
||
Consider a case where you want to return owned data from a method, but you | ||
don't want that data to live longer than the value that created it. | ||
|
||
- Lifetimes need to come from somewhere! We can't build functions of the form | ||
`fn lifetime_shenanigans<'a>(owned: OwnedData) -> &'b Data` (without tying | ||
`'b` to `'a` in some way). | ||
|
||
Lifetime elision hides where a lot of lifetimes come from, but that doesn't | ||
mean the explicitly named lifetimes "come from nowhere." | ||
|
||
Suggestion: Show off un-eliding the lifetimes in `get_erased` in this example. | ||
|
||
- [`BorrowedFd`](https://rust-lang.github.io/rfcs/3128-io-safety.html#ownedfd-and-borrowedfdfd) | ||
uses these captured lifetimes to enforce the invariant that "if this file | ||
descriptor exists, the OS file descriptor is still open" because a | ||
`BorrowedFd`'s lifetime parameter demands that there exists another value in | ||
your program that has the same lifetime as it, and this has been encoded by | ||
the API designer to mean _that value is what keeps the access to the file | ||
open_. | ||
|
||
Its counterpart `OwnedFd` is instead a file descriptor that closes that file | ||
on drop. | ||
|
||
- This way of encoding information in types is _exceptionally powerful_ when | ||
combined with unsafe, as the ways one can manipulate lifetimes becomes almost | ||
arbitrary. This is also dangerous, but when combined with tools like external, | ||
mechanically-verified proofs _we can safely encode cyclic/self-referential | ||
types while encoding lifetime & safety expectations in the relevant data | ||
types._ | ||
|
||
The [GhostCell (2021)](https://plv.mpi-sws.org/rustbelt/ghostcell/) paper and | ||
its [relevant implementation](https://gitlab.mpi-sws.org/FP/ghostcell) show | ||
this kind of work off. While the borrow checker is restrictive, there are | ||
still ways to use escape hatches and then _show that the ways you used those | ||
escape hatches are consistent and safe._ | ||
|
||
</details> |
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Uh oh!
There was an error while loading. Please reload this page.