From 160e36168928c2b5342de7ddcfa64aa22d09d8e1 Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Mon, 5 Aug 2019 10:57:52 +0200 Subject: [PATCH 1/6] define (un)sound --- reference/src/glossary.md | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/reference/src/glossary.md b/reference/src/glossary.md index 5d1fedbd..16366183 100644 --- a/reference/src/glossary.md +++ b/reference/src/glossary.md @@ -146,6 +146,11 @@ Moreover, such unsafe code must not return a non-UTF-8 string to the "outside" o To summarize: *Data must always be valid, but it only must be safe in safe code.* For some more information, see [this blog post](https://www.ralfj.de/blog/2018/08/22/two-kinds-of-invariants.html). +#### Soundness (of code / of a library) + +We say that a library (can be an individual function) is *sound* if it is impossible for safe code to cause Undefined Behavior using its public API. +Conversely, the library is *unsound* if safe code *can* cause Undefined Behavior. + #### Layout The *layout* of a type defines its size and alignment as well as the offsets of its subobjects (e.g. fields of structs/unions/enum/... or elements of arrays). From e8860ce6704adba37aaa5234cde4974527bff0fa Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Mon, 5 Aug 2019 20:06:59 +0200 Subject: [PATCH 2/6] less awkward --- reference/src/glossary.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/reference/src/glossary.md b/reference/src/glossary.md index 16366183..2f1f0e13 100644 --- a/reference/src/glossary.md +++ b/reference/src/glossary.md @@ -148,8 +148,8 @@ For some more information, see [this blog post](https://www.ralfj.de/blog/2018/0 #### Soundness (of code / of a library) -We say that a library (can be an individual function) is *sound* if it is impossible for safe code to cause Undefined Behavior using its public API. -Conversely, the library is *unsound* if safe code *can* cause Undefined Behavior. +We say that a library (or an individual function) is *sound* if it is impossible for safe code to cause Undefined Behavior using its public API. +Conversely, the library/function is *unsound* if safe code *can* cause Undefined Behavior. #### Layout From f7a0a3a8a92e8601935374f32e2392b7dac17c1d Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Tue, 6 Aug 2019 10:47:18 +0200 Subject: [PATCH 3/6] use soundness in explaining the safety invariant --- reference/src/glossary.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/reference/src/glossary.md b/reference/src/glossary.md index 2f1f0e13..3adffc87 100644 --- a/reference/src/glossary.md +++ b/reference/src/glossary.md @@ -129,7 +129,7 @@ fn main() { unsafe { The *safety* invariant is an invariant that safe code may assume all data to uphold. This invariant is used to justify which operations safe code can perform. The safety invariant can be temporarily violated by unsafe code, but must always be upheld when interfacing with unknown safe code. -It is not relevant when arguing whether some *program* has UB, but it is relevant when arguing whether some code safely encapsulates its unsafety -- IOW, it is relevant when arguing whether some *library* can be used by safe code to *cause* UB. +It is not relevant when arguing whether some *program* has UB, but it is relevant when arguing whether some code safely encapsulates its unsafety -- IOW, it is relevant when arguing whether some *library* is [sound][soundness] In terms of code, some data computed by `TERM` (possibly constructed from some `arguments` that can be *assumed* to satisfy the safety invariant) is valid at type `T` if and only if the following library function can be safely exposed to arbitrary (safe) code as part of the public library interface: ```rust,ignore @@ -147,6 +147,7 @@ To summarize: *Data must always be valid, but it only must be safe in safe code. For some more information, see [this blog post](https://www.ralfj.de/blog/2018/08/22/two-kinds-of-invariants.html). #### Soundness (of code / of a library) +[soundness]: #soundness-of-code--of-a-library We say that a library (or an individual function) is *sound* if it is impossible for safe code to cause Undefined Behavior using its public API. Conversely, the library/function is *unsound* if safe code *can* cause Undefined Behavior. From 849d3bf5c4156b56a10d4d51b3caa9139de7339f Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Tue, 6 Aug 2019 21:14:34 +0200 Subject: [PATCH 4/6] define UB and give some context to soundness --- reference/src/glossary.md | 20 +++++++++++++++++++- 1 file changed, 19 insertions(+), 1 deletion(-) diff --git a/reference/src/glossary.md b/reference/src/glossary.md index 3adffc87..76e9578a 100644 --- a/reference/src/glossary.md +++ b/reference/src/glossary.md @@ -146,10 +146,28 @@ Moreover, such unsafe code must not return a non-UTF-8 string to the "outside" o To summarize: *Data must always be valid, but it only must be safe in safe code.* For some more information, see [this blog post](https://www.ralfj.de/blog/2018/08/22/two-kinds-of-invariants.html). +#### Undefined Behavior +[ub]: #undefined-behavior + +*Undefined Behavior* is a concept of the contract between the Rust programmer and the compiler: +The programmer promises that the code exhibits no undefined behavior. +In return, the compiler promises to compile the code in a way that the final program does on the real hardware what the source program does according to the Rust Abstract Machine. +If it turns out the program *does* have undefined behavior, the contract is void, and the program produced by the compiler is essentially garbage (in particular, it is not bound by any specification; the program does not even have to be well-formed executable code). + +In Rust, the [Nomicon](https://doc.rust-lang.org/nomicon/what-unsafe-does.html) and the [Reference](https://doc.rust-lang.org/reference/behavior-considered-undefined.html) both have a list of behavior that the language considers undefined. +Rust promises that safe code cannot cause Undefined Behavior---it takes the burden of this contract on itself. +For unsafe code, however, the burden is still on the programmer. + +Also see: [Soundness][soundness]. + #### Soundness (of code / of a library) [soundness]: #soundness-of-code--of-a-library -We say that a library (or an individual function) is *sound* if it is impossible for safe code to cause Undefined Behavior using its public API. +*Soundness* is a type system concept (actually originating from the study of logics) and means that the type system is "correct" in the sense that well-typed programs actually have the desired properties. +For Rust, this means well-typed programs cannot cause [Undefined Behavior][ub]. +This promise only extends to safe code however; for `unsafe` code, it is up to the programmer to uphold this contract. + +Accordingly, we say that a library (or an individual function) is *sound* if it is impossible for safe code to cause Undefined Behavior using its public API. Conversely, the library/function is *unsound* if safe code *can* cause Undefined Behavior. #### Layout From 7c04179fbc70cb9b737a81b1b9839639fb2b56c7 Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Wed, 7 Aug 2019 10:48:21 +0200 Subject: [PATCH 5/6] Full stop Co-Authored-By: Mazdak Farrokhzad --- reference/src/glossary.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/reference/src/glossary.md b/reference/src/glossary.md index 76e9578a..505cb935 100644 --- a/reference/src/glossary.md +++ b/reference/src/glossary.md @@ -129,7 +129,7 @@ fn main() { unsafe { The *safety* invariant is an invariant that safe code may assume all data to uphold. This invariant is used to justify which operations safe code can perform. The safety invariant can be temporarily violated by unsafe code, but must always be upheld when interfacing with unknown safe code. -It is not relevant when arguing whether some *program* has UB, but it is relevant when arguing whether some code safely encapsulates its unsafety -- IOW, it is relevant when arguing whether some *library* is [sound][soundness] +It is not relevant when arguing whether some *program* has UB, but it is relevant when arguing whether some code safely encapsulates its unsafety -- IOW, it is relevant when arguing whether some *library* is [sound][soundness]. In terms of code, some data computed by `TERM` (possibly constructed from some `arguments` that can be *assumed* to satisfy the safety invariant) is valid at type `T` if and only if the following library function can be safely exposed to arbitrary (safe) code as part of the public library interface: ```rust,ignore From 53aec0bece3bea1390bdd781f72d8a12e71e39e2 Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Thu, 15 Aug 2019 13:18:33 +0200 Subject: [PATCH 6/6] compiler and unsafe code authors share this burden --- reference/src/glossary.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/reference/src/glossary.md b/reference/src/glossary.md index 505cb935..520d5591 100644 --- a/reference/src/glossary.md +++ b/reference/src/glossary.md @@ -129,7 +129,7 @@ fn main() { unsafe { The *safety* invariant is an invariant that safe code may assume all data to uphold. This invariant is used to justify which operations safe code can perform. The safety invariant can be temporarily violated by unsafe code, but must always be upheld when interfacing with unknown safe code. -It is not relevant when arguing whether some *program* has UB, but it is relevant when arguing whether some code safely encapsulates its unsafety -- IOW, it is relevant when arguing whether some *library* is [sound][soundness]. +It is not relevant when arguing whether some *program* has UB, but it is relevant when arguing whether some code safely encapsulates its unsafety -- in other words, it is relevant when arguing whether some *library* is [sound][soundness]. In terms of code, some data computed by `TERM` (possibly constructed from some `arguments` that can be *assumed* to satisfy the safety invariant) is valid at type `T` if and only if the following library function can be safely exposed to arbitrary (safe) code as part of the public library interface: ```rust,ignore @@ -155,7 +155,7 @@ In return, the compiler promises to compile the code in a way that the final pro If it turns out the program *does* have undefined behavior, the contract is void, and the program produced by the compiler is essentially garbage (in particular, it is not bound by any specification; the program does not even have to be well-formed executable code). In Rust, the [Nomicon](https://doc.rust-lang.org/nomicon/what-unsafe-does.html) and the [Reference](https://doc.rust-lang.org/reference/behavior-considered-undefined.html) both have a list of behavior that the language considers undefined. -Rust promises that safe code cannot cause Undefined Behavior---it takes the burden of this contract on itself. +Rust promises that safe code cannot cause Undefined Behavior---the compiler and authors of unsafe code takes the burden of this contract on themselves. For unsafe code, however, the burden is still on the programmer. Also see: [Soundness][soundness].