-
Notifications
You must be signed in to change notification settings - Fork 16
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
Atomic Types Challenge #82
base: main
Are you sure you want to change the base?
Conversation
|
||
In addition to any properties called out as SAFETY comments in the source code, all proofs must automatically ensure the absence of the following [undefined behaviors](https://github.com/rust-lang/reference/blob/142b2ed77d33f37a9973772bd95e6144ed9dce43/src/behavior-considered-undefined.md): | ||
|
||
* Data races. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Note that adding data races means that we cannot complete this challenge with Kani. I can take this out if we'd prefer to leave data races out of scope for this challenge. Not sure the feasibility of adding a tool later that can reason about this.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The underlying CBMC supports concurrency, so perhaps Kani can do it?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think in principle we should keep this, since that is the main safety property of many safety guarantees offered by the type.
It's not clear to me what forms these proofs would take.
|
||
In addition to any properties called out as SAFETY comments in the source code, all proofs must automatically ensure the absence of the following [undefined behaviors](https://github.com/rust-lang/reference/blob/142b2ed77d33f37a9973772bd95e6144ed9dce43/src/behavior-considered-undefined.md): | ||
|
||
* Data races. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The underlying CBMC supports concurrency, so perhaps Kani can do it?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks @carolynzech! Is there any usage of the unsafe functions in the standard library that is worth including in the challenge?
|
||
In addition to any properties called out as SAFETY comments in the source code, all proofs must automatically ensure the absence of the following [undefined behaviors](https://github.com/rust-lang/reference/blob/142b2ed77d33f37a9973772bd95e6144ed9dce43/src/behavior-considered-undefined.md): | ||
|
||
* Data races. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think in principle we should keep this, since that is the main safety property of many safety guarantees offered by the type.
It's not clear to me what forms these proofs would take.
- `atomic_umax` | ||
- `atomic_umin` | ||
|
||
These functions are wrappers around compiler intrinsics. Thus, your task is to ensure that we cannot cause undefined behavior by invoking the intrinsics on these inputs. For instance, if the intrinsic takes as input a raw pointer and reads the value at that pointer, your contracts should ensure that we would not cause UB by performing the read. For the purpose of this challenge, you may assume that any UB in the intrinsics would be a direct consequence of malformed inputs. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Maybe this challenge should include writing contracts for those intrinsics and ensuring that the contracts are not violated by these methods.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
See comment. I can add intrinsics to this challenge as well, although we may want to be mindful of length. If we have contracts on the methods, intrinsics, and a meatier standard library application, this challenge will likely be the longest one we have. That's not necessarily bad, but I wonder if atomic intrinsics would be better as a separate challenge to keep the size of this one more manageable.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The methods are safe though.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Sure, but we still want to verify unsafe code inside safe functions, no?
Yes. I was erring on the side of keeping this challenge smaller, but there's some libraries that use more of the methods than |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks @carolynzech
I just have a few suggestions about the wording.
However, you need not verify the method for all possible instantiations of `T`. | ||
It suffices to verify this method for `T` of byte sizes 0, 1, 2, 4, and at least one non-power of two. | ||
|
||
#### Part 2: Unsafe Atomic Functions |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Safe abstractions?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Not sure what this comment means -- are you asking me to change the title, or for something to be added?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
And/Or are you asking that that this part:
Also write contracts enforcing that the functions are not invoked with
order
s that would cause them to panic.
Be changed so that the contracts are on the safe abstractions (the methods) instead of the unsafe methods?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
For now, I added a new section called "Safe Abstractions" that changes the contracts about panicking to be on the safe methods. LMK if I misinterpreted.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Sorry, I'll try to be more specific next time. I was adding the comment while waiting to board my flight.
I meant that this section is named unsafe functions, but the target functions are in fact safe. Instead, this is about verifying the usage of unsafe inside the safe function. Safe functions that invoke unsafe are known as safe abstractions. Let me know if that makes sense
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Makes sense. Made some changes.
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.