Irc11 faa specs - #2872
Irc11 faa specs#2872elanortang wants to merge 8 commits into
Conversation
zero-to-nat
left a comment
zero-to-nat
left a comment
There was a problem hiding this comment.
Looks good, thank you for adding these specs! If possible, could you hold off on merging? I would like to add the remaining fetch_<op> specs, and then request a review from Hai on all of them.
| pub open spec fn load_acquire<T>( | ||
| pt: AtomicPointsTo<T>, | ||
| old_view: ThreadView, | ||
| new_view: ThreadView, | ||
| val: T, | ||
| timestamp: nat, | ||
| message_view: ThreadView, | ||
| ) -> bool { | ||
| &&& load_timestamp_in_view(pt, old_view, new_view, timestamp) | ||
| &&& load_reads_from_history(pt.hist(), val, timestamp, message_view) | ||
| &&& load_view_nondecreasing( | ||
| old_view, | ||
| new_view, | ||
| ) | ||
| // because this is an acquire load, the message view is joined to the thread's current view | ||
| &&& new_view.contains(message_view) | ||
| } |
There was a problem hiding this comment.
not related to the PR, but:
It seems you don't need acquire_view here, so you probably don't need to maintain that acquire_view.contains(new_view)?
It seems that you also only use release_view as input and acquire_view as output (no old and new views)
There was a problem hiding this comment.
Sorry, I'm not sure I understand yet what you mean. In this spec fn, old_view is intended to be the thread's current view before the atomic op, and new_view is the thread's current view after the atomic op. I didn't intend for this spec to deal with acquire views, since it is an acquire load. (In contrast, load_relaxed does have something to say about the acquire view).
Perhaps I am using this spec in a place where the new_view argument is from an AcquireViewSeen? If so, that is probably a mistake.
There was a problem hiding this comment.
I think my question is about how you update the release view or the acquire view after the step.
oRC11 maintains the property that release_view ⊑ current_view ⊑ acquire_view, so when it updates the release view, it applies the same update to the current and acquire view, and similarly when updating the current view, it applies the same update to the acquire view. This is encapsulated in the 𝒱 → 𝒱' relation.
I think for the existing examples this property may not be needed, and it is sound to track a smaller view then the current view or acquire view actually is (you can only do less with smaller views).
There was a problem hiding this comment.
I see, thank you for the clarification!
We do not explicitly track the exact release/current/acquire views of each thread. Owning a ViewSeen can be thought of as having a lower bound on the owning thread's current view -- the actual view may be larger. Similarly for the AcquireViewSeen and ReleaseViewSeen permissions.
Since (based on my understanding) an acquire read doesn't add anything to the acquire view that is not also added to the current view, I don't think we need to specify anything extra about the acquire view here.
In terms of the property: release_view ⊑ current_view ⊑ acquire_view, I suppose we could introduce an axiom cur_to_acq(vs: ViewSeen) -> (acq_vs: AcquireViewSeen) ensures vs@ == acq_vs@. But I'm not sure where that would be useful.
| pub open spec fn load_view_nondecreasing(old_view: ThreadView, new_view: ThreadView) -> bool { | ||
| new_view.contains(old_view) | ||
| } |
There was a problem hiding this comment.
also not related to the PR: why can't this be inlined? what's the purpose of having it as a separate spec fn?
There was a problem hiding this comment.
Good point, I think this was intended mostly for readability inside the load_acquire and load_relaxed specs. But now I am realizing that this is actually redundant in load_acquire!
| up.store_message_view, | ||
| ) | ||
| }, | ||
| _ => true, |
There was a problem hiding this comment.
shouldn't this be false? Assuming that we're not allowing SC. If you want to allow for SC, it should be the same case with Ordering::AcqRel
| up.load_timestamp, | ||
| up.load_message_view, | ||
| ), | ||
| _ => true, |
This branch has not been deployed
3 participants
Add specs for
fetch_add_wrapping,fetch_sub_wrapping,fetch_and,fetch_or,fetch_xor,fetch_nand,fetch_min,fetch_max,compare_exchange_weak,swap.By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.