Acyclic
| pub unsafe trait Acyclic {} | |
| // struct Rc<T: RcSafe> | |
| // struct Arc<T: RcSafe> | |
| // R1: structural | |
| unsafe impl Acyclic for .. {} | |
| // R2: no-ownership | |
| unsafe impl<T> Acyclic for Weak<T> {} | |
| unsafe impl<T: Copy> Acyclic for T {} // assuming we actually prohibit Copy+Drop | |
| unsafe impl<'a, T> Acyclic for &'a mut T {} | |
| // R3R: RefCell-inductive | |
| unsafe impl<T> !Acyclic for RefCell<T> {} | |
| #[inductive] | |
| unsafe impl<T: Acyclic> Acyclic for RefCell<T> {} | |
| // R3M: Mutex-inductive | |
| unsafe impl<T> !Acyclic for Mutex<T> {} | |
| #[inductive] | |
| unsafe impl<T: Acyclic> Acyclic for Mutex<T> {} |
| The invariant is that a type is Acyclic if it can't be part of an owning reference cycle. | |
| If T can't be a part of a reference cycle, then RefCell<T> (or Mutex<T>) also can't be part of one. this justifies R3: inductive. | |
| If T isn't RefCell or Mutex, then T can't be constructed as part of a reference cycle. It can only become a part of a cycle if it refers to a RefCell or Mutex that can be part of a cycle. However, if T is Acyclic and refers to a RefCell, by inductivity we know that the RefCell is already not part of a cycle. This justifies R1: structural. | |
| Non-owning references can never be part of a cycle. This justifies R2: no-ownership. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment