Skip to content
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

UnsafeCell should implement the Copy trait #25053

Open
diwic opened this Issue May 2, 2015 · 51 comments

Comments

Projects
None yet
@diwic
Copy link
Contributor

diwic commented May 2, 2015

Currently UnsafeCell does not implement Copy. It would be beneficial if it could, for at least two reasons:

  • Easier initialization of fixed arrays, e g: [UnsafeCell::new(0i32); 75]
  • It enables people to make cell-like types which are Copy.

AFAIK, there are no disadvantages for UnsafeCell to implement Copy.

Note: the reason people can't just copy-and-paste the code for UnsafeCell to make their own variant with copy semantics, is that UnsafeCell is a #[lang="unsafe_cell"]: "The UnsafeCell<T> type is the only legal way to obtain aliasable data that is considered mutable. In general, transmuting an &T type into an &mut T is considered undefined behavior."

@mattico

This comment has been minimized.

Copy link
Contributor

mattico commented May 2, 2015

This seems like it would require an RFC:
Any semantic or syntactic change to the language that is not a bugfix.
https://github.com/rust-lang/rfcs

@steveklabnik steveklabnik added the A-libs label May 2, 2015

@P1start

This comment has been minimized.

Copy link
Contributor

P1start commented May 2, 2015

@mattico Making UnsafeCell implement Copy isn’t a change to the language, it’s a change to the standard library. The rules for what requires an RFC aren’t very clear, anyway.

@reem

This comment has been minimized.

Copy link
Contributor

reem commented May 3, 2015

If adding a trait impl to a type required an RFC we would never get anything done.

@alexcrichton

This comment has been minimized.

Copy link
Member

alexcrichton commented May 3, 2015

There is currently no stable and safe method to read the value in an UnsafeCell, and this is intentional. There is no knowledge about concurrent reads/writes/etc with an UnsafeCell, and introducing an unsynchronized read with an implicit Copy may produce undefined behavior in some situations.

@diwic

This comment has been minimized.

Copy link
Contributor Author

diwic commented May 3, 2015

@alexcrichton UnsafeCell is a building block for higher level abstractions, e g Cell, RefCell and AtomicUsize. This higher level abstraction determines whether unsynchronized reads are possible or not, by optionally deriving Copy (and/or Send/Sync) themselves. (Or by adding NoCopy markers.)
If UnsafeCell implements Copy, then the higher level abstractions are free to make this choice. The current situation makes this impossible.

Could you be more specific about the "undefined behavior in some situations"? And is this a problem with UnsafeCell in itself, or something that can be easily fixed in the type containing the UnsafeCell?

@alexcrichton

This comment has been minimized.

Copy link
Member

alexcrichton commented May 4, 2015

Yes each type which contains an UnsafeCell could also take on deciding these kinds of decisions, there's no absolutely fundamental reason why it does not implement Copy.

@diwic

This comment has been minimized.

Copy link
Contributor Author

diwic commented Jun 2, 2015

I was thinking about this again today and I'm wondering if it would be better to remove the unsafe_cell lang_item and instead introduce a new marker, e g AliasedMutRef or so, that would mean essentially the same (disable the assumption/optimisation that two mutable references can never refer to the same object)?

Then people could implement their own cells with what ever degree of unsafety they want.

@nox

This comment has been minimized.

Copy link
Contributor

nox commented May 5, 2016

We need this for FFI with C and C++ too, where it would be nice to be able to tell that some struct fields may change through unknown means.

@arielb1

This comment has been minimized.

Copy link
Contributor

arielb1 commented May 5, 2016

+1

@aturon

This comment has been minimized.

Copy link
Member

aturon commented May 5, 2016

Nominating for libs team discussion.

@alexcrichton

This comment has been minimized.

Copy link
Member

alexcrichton commented May 11, 2016

This libs team discussed this issue a few days ago and we unfortunately didn't reach a firm consensus. The case I mentioned above means that guaranteeing the safety of an unsafe block with an UnsafeCell would not also entail auditing all copies in addition to accesses. This does, however, somewhat align with the desire for safe methods like get_mut (to get a &mut T reference).

One idea brought up by @sfackler was perhaps something like unsafe impl Copy for T {} where the type T is then copyable regardless of contents (but is clearly unsafe, hence the requirement of unsafe). This idea hasn't been played out too much, though, and would certainly require an RFC.

One other concern here is that if UnsafeCell implements Copy that it would also necessitate an implementation of Clone, which may be more dubious.

@comex

This comment has been minimized.

Copy link
Contributor

comex commented Nov 27, 2016

Just ran into this.

@alexcrichton Can you think of any other cases in which it would make sense to unsafe impl Copy for something with a non-Copy field? Maybe something involving unions? I can't think of anything concrete.

If there aren't any, then special syntax seems unwarranted; if UnsafeCell shouldn't impl Copy, seems easiest to just create a second type that acts the same but does.

@comex

This comment has been minimized.

Copy link
Contributor

comex commented Dec 11, 2016

Another possible use case for unsafe impl Copy: bluss/arrayvec#32

Though it probably wouldn't be the best approach in that case. In short, ArrayVec is a Vec-like type backed by an inline [NoDrop<T>; N]. In general it needs a Drop impl to manually drop only elements up to len(), but ideally an ArrayVec with Copy elements would be Copy. One potential way to do that would be a hypothetical unsafe impl Copy that worked for types with Drop. Probably a superior approach would involve some way to bound the Drop impl on !Copy, though.

@diwic

This comment has been minimized.

Copy link
Contributor Author

diwic commented Dec 11, 2016

If it makes things easier, we could make an additional type CopyUnsafeCell (name to be bikeshedded), which is the lang item and implements copy (and a clone, which just does bit-copy), and then the UnsafeCell which wraps CopyUnsafeCell would just change its implementation to call CopyUnsafeCell, and it would automatically disable copy (by not deriving it).

As additional bonus, our regular Cell could then wrap CopyUnsafeCell instead of the current non-copy UnsafeCell and we'll be able to do [Cell::new(6u8); 1000].

@aturon

This comment has been minimized.

Copy link
Member

aturon commented Jan 4, 2017

cc @rust-lang/lang, anybody on the lang team have an opinion on this?

@nikomatsakis

This comment has been minimized.

Copy link
Contributor

nikomatsakis commented Jan 4, 2017

I am in favor. UnsafeCell is a building block. It should be possible for people to build Copy types that use it if they so choose.

@nikomatsakis

This comment has been minimized.

Copy link
Contributor

nikomatsakis commented Jan 4, 2017

Discussed this a bit with @aturon -- I agree with the consensus that it would be easy to write broken code if UnsafeCell: Copy. Something like unsafe impl Copy is also appealing as an alternative.

This reminds me of the discussion around a Pod trait, which was supposed to be for "things that could be copy, but where copying is likely a bug". We would up at that time deciding against it -- having a trait made for a lot of sharp edges iirc -- but thinking that bugs might be well served by something analogous to the #[must_use] lint, which could warn about implicit copies of things you don't want to copy.

Still, I feel like while having implicit copies might be dangerous from a race condition POV, it's also easy to imagine types that wouldn't have to worry about that. If my type is not Sync, for example, then it is fine to copy the data in the UnsafeCell. FFI might be another example.

@aturon

This comment has been minimized.

Copy link
Member

aturon commented Jan 21, 2017

This issue seems to be at a bit of a standstill.

  • On the one hand, there's a legit need for a Copy version of UnsafeCell, for things like FFI.
  • On the other hand, making UnsafeCell itself Copy is a potential footgun.

If we want to deal with both of these perspectives, we can rule out changing UnsafeCell itself. That leaves us with at least two options mentioned so far:

  • Providing a separate version of UnsafeCell that is copy (perhaps VeryUnsafeCell 😉)
  • Adding a mechanism like unsafe impl Copy

The former is clearly the easier approach, and personally I'm hesitant to add special casing to the handling of Copy impls just for this particular case.

Does anyone strongly object to adding some additional version of UnsafeCell that is Copy?

@nox

This comment has been minimized.

Copy link
Contributor

nox commented Jan 21, 2017

Doesn't VeryUnsafeCell mean yet another ad-hoc language item?

@eddyb

This comment has been minimized.

Copy link
Member

eddyb commented Jan 21, 2017

I thought @nikomatsakis had some more usecases for unsafe impl Copy in mind.

@diwic

This comment has been minimized.

Copy link
Contributor Author

diwic commented Jan 22, 2017

@nox, if VeryUnsafeCell will be the new lang item and UnsafeCell is just a non-copy wrapper around that, then the total amount of lang items remains unchanged.

@diwic

This comment has been minimized.

Copy link
Contributor Author

diwic commented Jan 22, 2017

For name bikeshedding, how about RawUnsafeCell?

@alexcrichton

This comment has been minimized.

Copy link
Member

alexcrichton commented Jan 22, 2017

@aturon I feel that adding a new type wouldn't actually solve the problem the problem I raised earlier. That'd still be a problem for anyone using VeryUnsafeCell, and presumably a bunch of types would want to move over to using that.

In that sense then if we must solve this specific issue then I'd be in favor of just adding the impl to UnsafeCell itself. Ideally we could find a totally separate route for solving this issue, but I'm not sure that's possible.

@comex

This comment has been minimized.

Copy link
Contributor

comex commented Jan 23, 2017

@alexcrichton Which types do you think would want to move over? As I see it, the only reason to use VeryUnsafeCell would be if you want your type to be Copy.

In any case, UnsafeCell is already !Sync; assuming VeryUnsafeCell is too, a naive user of UnsafeCell will be blocked from accessing it from multiple threads to start with. To get a bug, you need to either unsafe impl Sync or do something unsafe with FFI, e.g. calling a C function that writes to the pointer from another thread. The former is asking for trouble, and the latter is not really an UnsafeCell-specific problem (there are all sorts of ways to create footguns out of C functions with weird semantics).

@alexcrichton

This comment has been minimized.

Copy link
Member

alexcrichton commented Jan 23, 2017

Well presumably there's some motivation for some type that wants to move over, right? Otherwise this issue wouldn't exist? We may not have cases in the standard library itself but I would hate to have a convention of "use UnsafeCell but if you're serious use VeryUnsafeCell"

@comex

This comment has been minimized.

Copy link
Contributor

comex commented Jan 23, 2017

IMO, VeryUnsafeCell is probably the wrong name. If there is a separate type, it should be specifically for Copy and named as such, e.g. CopyUnsafeCell. It's not just a generic 'more low-level' version.

When it comes to motivations, I'm not totally sure it's wrong to just mark both UnsafeCell and Cell as Copy. If I have Vec<Cell<u8>>, it really should be eligible for copy_from_slice. If I have a Cell in my struct, it should still be usable in copy_arena::Arena and other APIs that require Copy for bookkeeping purposes (though arguably a better solution in this case could be to have a "trivial drop" auto trait separate from Copy). But... if this is considered inadvisable, the only option is for me to make my own version of Cell, for which I cannot avoid UnsafeCell for the reasons specified in the original post.

(sidenote: if UnsafeCell because a wrapper, people might be tempted to avoid it to improve the experience in a debugger, where at least IME you often have to manually traverse wrapper structs. Maybe #[repr(transparent)] could help with this? Or just use two lang items instead of a wrapper. Ultimately the 'right' solution is to build rustc and Rust syntax into the debugger so you can just use the normal accessor methods, but that's probably a long way off.)

@aturon

This comment has been minimized.

Copy link
Member

aturon commented Jan 24, 2017

@comex

IMO, VeryUnsafeCell is probably the wrong name.

To be clear, it was mentioned as a joke :)

I'm not totally sure it's wrong to just mark both UnsafeCell and Cell as Copy

The problem is with the potential for implicit reads leading to data races.

@alexcrichton

That'd still be a problem for anyone using VeryUnsafeCell, and presumably a bunch of types would want to move over to using that.

I agree that it's still a problem for the new type, but I'm not sure how often it'd be used (and we can warn strongly against it).

Also, despite there still being that potential footgun, the problem in my mind is that you simply cannot get the desired functionality today. That is, if you want a structure that is both Copy and contains an UnsafeCell, you're just out of luck. And I think that's a legitimate thing to sometimes want.

@withoutboats

This comment has been minimized.

Copy link
Contributor

withoutboats commented Jan 24, 2017

You can't use it as a generic T: Copy, but in terms of performance you can provide a clone impl that just memcopies can't you? I don't understand the FFI use case.

@comex

This comment has been minimized.

Copy link
Contributor

comex commented Jan 24, 2017

@aturon Er, thinko on my part. What I meant to write is not that it shouldn't literally be called VeryUnsafeCell, but that that's the wrong basis for a name, I.e. the idea of being a generic 'lower-level UnsafeCell', as opposed to something with a specific use case in mind.

Regarding making existing types Copy, to elaborate: I understand the worry about data races, but I'm not so sure it's likely to cause errors in practice. Cell Itself is not really intended to be wrapped in Sync types at all; UnsafeCell is, but most code using UnsafeCell is probably generic and thus can't implicitly copy anyway. And I can't easily imagine what sort of code would accidentally copy the entire cell.

@nikomatsakis

This comment has been minimized.

Copy link
Contributor

nikomatsakis commented Jan 24, 2017

I agree that extending the language just for this case seems odd, but it also seems odd that you can "opt out" of the safety for Send and Sync but not Copy. That said I don't have other specific use-cases in mind yet.

@steveklabnik steveklabnik removed the A-libs label Mar 24, 2017

@ubsan

This comment has been minimized.

Copy link
Contributor

ubsan commented Jul 20, 2017

This seems strange. I don't understand why y'all are so cautious to implement Copy for UnsafeCell. There's no safe way to do reads or writes on an UnsafeCell, and it isn't Sync, so there are no issues with unsynchronized reads. If you're doing unsynchronized writes to an UnsafeCell, you've written a bad Sync wrapper for UnsafeCell, and it's pretty trivial to break UnsafeCell with unsafe code anyways. Otherwise, it's impossible to cause UB with a Copy UnsafeCell.

Basically, I don't understand the footgun here - there is none without writing code that is already broken without Copy.

@ubsan

This comment has been minimized.

Copy link
Contributor

ubsan commented Jul 20, 2017

(Also, you know, UnsafeCell is an unsafe building block with Unsafe in the name. It screams "be careful!", unlike, say, transmute. cough.)

@aturon

This comment has been minimized.

Copy link
Member

aturon commented Jul 20, 2017

@ubsan The problem is that the copy is done implicitly, making it easy for there to be a read you don't realize is happening.

@pythonesque

This comment has been minimized.

Copy link
Contributor

pythonesque commented Jul 20, 2017

@withoutboats The problem is that the Copy bound is special cased for a lot of stuff that is not easy to replicate with clone(), since it's known not to have a nontrivial destructor (among other things). The issue isn't performance; there are plenty examples above demonstrating the issue. Something like Pod would be preferable, but I'm not sure it would be easy to add at this point.

Either way, as long as we're trying to make UnsafeCell a requirement for many kinds of unsafe idioms, not allowing it to be Copy is pretty silly. The potential for data races is there, but you would have to write unsafe code to get that behavior (specifically, you'd have to opt into Sync, which already leads to data races both in theory and practice when you're not careful). Moreover, since Copy has to be explicitly derived, there shouldn't be a single example of code that's correct today that would be broken if UnsafeCell was Copy. And, frankly: even if an UnsafeCell is present in a Sync data structure, that still doesn't mean it shouldn't be Copy! The UnsafeCell may only be used during initialization, or when the value is not shared with other threads. I think the footgun potential here is being grossly overstated.

@pythonesque

This comment has been minimized.

Copy link
Contributor

pythonesque commented Jul 20, 2017

@aturon If the usual synchronization primitives (including atomics) opt out, how likely is it that people will actually be trying to race on a straight-up UnsafeCell, though? I'd imagine it's rare for people to directly call the atomic intrinsics (especially on generic data structures, since at least last time I tried it they only sorta work on those), and without them it's kind of hard to come up with scenarios where you would be correct without a Copy but incorrect with one. And not only that, but the overall data type would have to have a trivial destructor.

I think this set of requirements (explicitly opt into Sync, trivial destructor, non-generic, using synchronization intrinsics explicitly [so you'd be racing correctly without Copy]) basically reduces you to reimplementations of atomics where you decide to #[derive(Copy)] which is surely pretty rare given that there are already correct ones in the standard library.

(Worth noting that this even applies to pointers, thanks to AtomicPtr).

@pythonesque

This comment has been minimized.

Copy link
Contributor

pythonesque commented Jul 20, 2017

Also! Being able to byte-copy something when it's not shared really is a different use case from being able to byte-copy something when it's shared, and there should probably be a way to differentiate them. It is annoying that one can't easily allocate fixed-size arrays of atomics, since (1) that's a very common thing to want to do and (2) the copies are perfectly safe, since there's no sharing until the array initialization is finished. Copy is clearly a subtype of that hypothetical trait, since you can always share something you own. And I believe assigning that trait to UnsafeCell (CopyOwn) would have no footguns at all, right? You could also assign Cell<T> where T : CopyOwn CopyOwn, since copying an unshared Cell would be perfectly valid as long as the contents were not shared; this could be seen as a further weakening of the existing MoveCell stuff.

(In general, I guess the analogy here would be Send:Sync as CopyOwn:Copy? This doesn't really work though, since it's not the case that T : Copy <-> &T : CopyOwn; perhaps instead this is closer to the original idea for Send and Sync, where &mut T => T copyable <-> T : CopyOwn and &T => T copyable <-> T Copy, since in this case Copy would still be a subtype of CopyOwn [as you can always get &T from &mut T]).

I guess my followup question would be: can anyone think of a reason they'd want to use UnsafeCell where CopyOwn was not sufficient (i.e., where you want full-blown Copy)? I think I still can (the "UnsafeCell is only written to at times when a race is impossible" case, which in a single-threaded context doesn't necessarily correspond to times that the UnsafeCell is uniquely owned) so the need for something like CopyOwn is probably a completely distinct issue.

@aturon

This comment has been minimized.

Copy link
Member

aturon commented Jul 20, 2017

@pythonesque

I'd imagine it's rare for people to directly call the atomic intrinsics (especially on generic data structures, since at least last time I tried it they only sorta work on those), and without them it's kind of hard to come up with scenarios where you would be correct without a Copy but incorrect with one.

Wow. That is an excellent point. @alexcrichton, thoughts?

@ubsan

This comment has been minimized.

Copy link
Contributor

ubsan commented Jul 21, 2017

@pythonesque you'd have to implement CopyOwn as some kind of Duplicate

fn duplicate(self) -> (Self, Self)

@aturon

This comment has been minimized.

Copy link
Member

aturon commented Jul 21, 2017

@RalfJung, I'd be curious to get your thoughts here as well.

@alexcrichton

This comment has been minimized.

Copy link
Member

alexcrichton commented Jul 21, 2017

Thanks for the comments @pythonesque! I don't think I quite understand the significance of the section @aturon quoted, but I think it makes sense to look at these concerns in real-world scenarios. For example I've used UnsafeCell a lot before in threaded contexts, but there's usually and AtomicUsize right next to it to guard access to the UnsafeCell. In that sense an outer #[derive(Copy)] would already be forbidden because the atomic isn't Copy. I think I'd be convinced on "this footgun exists but in practice rarely comes up".

One point, reading over this thread though, which was brought up earlier is that an implementation of Copy would necessitate an implementation of Clone. What would that look like?

@RalfJung

This comment has been minimized.

Copy link
Member

RalfJung commented Jul 21, 2017

@aturon here you go:

First of all, UnsafeCell is obviously not a safe abstraction, so it is a little hard to answer this question from a semantic perspective. Cell clearly could be copy (that's intuitively rather clear, it is !Sync, after all; also, we've proven this to be the case). For Cell to be Copy one day (if we ever want to do that), UnsafeCell needs to be Copy or there has to be an unsafe impl Copy.

I like @pythonesque's point about CopyOwn. Semantically speaking, T: Copy really provides two properties (and indeed, proving a type Copy in our formalism requires both of these to be established separately, neither of them sees to imply the other):

  1. If you own a T, you can copy the bytes and then you own two T. (Somewhat like @ubsan's duplicate, except that it's type is somewhat too weak -- you'd want to say that self does not get modified, and really moving your original T around is unnecessary operationally speaking.)
  2. If you have a shared T, i.e. if you own &T, you can dereference that pointer and make a copy of the bytes and you have a T.

From what I understand, CopyOwn is supposed to only provide the first guarantee. That sounds like a very reasonable thing to do for UnsafeCell; after all, UnsafeCell is only magic when shared, not when owned. Cell, RefCell, RwLock and friends could all be CopyOwn (if their inner type is). Maybe this is what the Pod trait was supposed to express?

The second guarantee, however, is a problem. Clearly many usecases of UnsafeCell violate it (RefCell and all the concurrency primitives come to my mind). @alexcrichton brought up the fact that Copy implies Clone, which is related to the second guarantee. UnsafeCell::clone sounds just wrong, that's a safe function that does unsynchronized reads from a shared UnsafeCell.

I like unsafe impl Copy independently of this because really, Copy is not all that different from Send and Sync -- they can all be satisfied for reasons the compiler does not understand. Maybe someone using Cell wants their type to be Copy; they would need such an unsafe impl.

However, CopyOwn/Pod can go way further than this -- most (all?) interior mutability types could be CopyOwn, which from what I understand would make more (like array initialization) compile and could even help performance. It also nicely aligns with our semantic model, so I'm a big fan of this right now. :D

@pythonesque

This comment has been minimized.

Copy link
Contributor

pythonesque commented Jul 21, 2017

Maybe we can get the best of all worlds like this, then:

  • CopyOwn can be propagated more or less automatically as Copy used to be (since the footgun potential is essentially nil, right?), which addresses the need to #[derive] constantly (note that we don't need to opt out for &T since &T being CopyOwn is not the same as T being Copy).
  • unsafe impl to opt into Copy for any CopyOwn type.
  • Use the above to change (most of) the compiler intrinsic stuff (like array allocation) that depends on Copy to depend on CopyOwn instead (except for explicitly copying through references, of course).
  • Also enable things like Copy for Cell where T : Copy.
  • Let library maintainers know that it's safe to switch things like copy_arena::Arena to use CopyOwn instead (since that will cover many more types).

It's late so I may be missing some stuff here, but I feel like this resolves pretty much all the Copy related stuff people want to do (well, other than non-trivial move implementations, but avoiding that has at least historically been an explicit goal of Rust's...).

@RalfJung

This comment has been minimized.

Copy link
Member

RalfJung commented Jul 21, 2017

I think there's still footgun potential. Imagine code like

let c = Cell::new(0);
let closure = || { /* using c */ }

If this used CopyOwn to make a copy, that's probably not what is intended.

@pythonesque

This comment has been minimized.

Copy link
Contributor

pythonesque commented Jul 21, 2017

Might it only do that if you explicitly said move?

(Actually, I think there's an argument that there should be an explicit copy required for CopyOwn stuff, if only we knew how to type it; we don't have "unique immutable reference" which is probably close to the right type).

@RalfJung

This comment has been minimized.

Copy link
Member

RalfJung commented Jul 21, 2017

Well, maybe, but this is exactly the kind of problem due to which Cell is not Copy, right?

@pythonesque

This comment has been minimized.

Copy link
Contributor

pythonesque commented Jul 21, 2017

I think Cell is not Copy because it currently can't be thanks to UnsafeCell.

@RalfJung

This comment has been minimized.

Copy link
Member

RalfJung commented Jul 22, 2017

I think ergonomics also played a rule, see my question from 2 years ago: https://users.rust-lang.org/t/why-is-cell-not-copy/2208

@pythonesque

This comment has been minimized.

Copy link
Contributor

pythonesque commented Jul 22, 2017

I find those examples very unconvincing, but why not make sure people are super explicit, then, and make the CopyMove Copy implementation activated in some super weird way (like creating a new array off of the base element)?

@ubsan

This comment has been minimized.

Copy link
Contributor

ubsan commented Jul 22, 2017

CopyOwn seems fine, but also... I'm not sure why we can't do both? It seems unreasonable, at least to me, to keep UnsafeCell from being Copy, given all the other arguments in this thread, and given that CopyOwn requires a lot of work (at least, I think).

@glaebhoerl

This comment has been minimized.

Copy link
Contributor

glaebhoerl commented Aug 21, 2017

@RalfJung

(and indeed, proving a type Copy in our formalism requires both of these to be established separately, neither of them sees to imply the other)

Could you explain how/why the second does not imply the first? Intuitively it seems to me that if you are given the ability to dereference an &T to make a new T (2.), then if you own a T (1.), you should be able to just make a reference to it (&T) and then invoke (2.).

@RalfJung

This comment has been minimized.

Copy link
Member

RalfJung commented Aug 21, 2017

Maybe that is an artifact of the framework we use for formalization. The reason is that (1) is an implication, saying that every possible way to justify the assertion "we own these bytes at type T" cannot possibly be making any exclusive "ownership"-style assumptions beyond owning these bytes. It has to all be duplicable. "ownership" here, as is common in correctness proofs of concurrent (and even sequential) programs, includes not only ownership of bytes in memory but also ownership of "ghost state", which is additional state that is tracked for the purpose of the proof but not actually present in the machine (e.g., this could be tracking which thread currently has "acquired" a RefCell even though no such tracking happens in the actual code). Property (2), on the other hand, is not a mere implication; we allow the proof of this to perform changes to the ghost state before producing a proof that the copy of the bytes is a new T. Since (1) must not make such changes, it cannot use (2).

Off the top of my head, I am not sure if we ever rely on (1) not making such changes. It certainly makes working with this much simpler though...

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.