fix(s2n-quic-platform): use custom storage type for messages #1807
Conversation
There was a problem hiding this comment.
re:UnsafeCells -- you probably know better than I if there's some kind of locking (semantic or through actual atomics etc) going on with &Header being converted to &mut Header. My current impression is that we always work with raw pointers if there's shared ownership (e.g., for the range of memory that is potentially shared with the kernel) and only convert to &Header and/or &mut Header if we have ownership of that region based on the start/end pointers and such.
Happy to sync up if this doesn't help explain my mental model enough.
camshaft
force-pushed
the
camshaft/ring-fixes
branch
2 times, most recently
from
6251aa0 to
367cd0c
Compare
|
Looks like the cmsg changes broke ECN... still investigating why |
camshaft
force-pushed
the
camshaft/ring-fixes
branch
from
09d5653 to
3d2bc2c
Compare
|
Alright; managed to get everything fixed! |
camshaft
force-pushed
the
camshaft/ring-fixes
branch
from
960cdbb to
42644eb
Compare
| @@ -16,17 +16,30 @@ fn main() -> Result<(), Error> { | |||
| } | |||
| } | |||
|
|
|||
| let is_miri = std::env::var("CARGO_CFG_MIRI").is_ok(); | |||
There was a problem hiding this comment.
You can't use cfg!(miri) for this?
There was a problem hiding this comment.
The cfg isn't passed to build scripts themselves, since they run on a different "platform" than the code that they're compiling.
| unsafe { libc::CMSG_SPACE(size_of::<T>() as _) as _ } | ||
| } | ||
|
|
||
| const fn const_max(a: usize, b: usize) -> usize { |
There was a problem hiding this comment.
I was going to suggest linking to rust-lang/rust#92391 in a TODO, but seems like that is going in a different direction anyway
|
|
||
| // This is currently needed due to how we detect if CMSG data has been written or not. | ||
| // | ||
| // TODO remove this once we split the `reset` traits into TX and RX types |
There was a problem hiding this comment.
Are you tracking this somewhere?
There was a problem hiding this comment.
It's in my later PRs so it's already done; just is waiting on deleting the socket v1
| // Applications should not cast it to a pointer type matching the | ||
| // payload, but should instead use memcpy(3) to copy data to or | ||
| // from a suitably declared object. | ||
| let data_ptr = cmsg_ptr.add(1); |
There was a problem hiding this comment.
not sure I'm following why its adding 1 here?
There was a problem hiding this comment.
It's what the CMSG_DATA function does, except ours is actually sound since we're not going from a *const to a *mut. I've including the call to CMSG_DATA in a debug_assertion to make sure they return the same thing.
| #[test] | ||
| #[cfg_attr(any(target_os = "linux", target_os = "android"), ignore)] // the linux implementation currently has an integer overflow on garbage data | ||
| #[cfg_attr(kani, kani::proof, kani::solver(cadical), kani::unwind(17))] |
There was a problem hiding this comment.
is cadical the go to now for Kani, or did you try kissat and it was slower?
There was a problem hiding this comment.
Cadical ended up being faster in this case. I think it just depends on the harness. The advantage cadical has is it's built in process to cbmc, as opposed to kissat that's an external binary. This forces cbmc to write a cnf to disk and then pass to kissat. Cadical APIs, instead, can just be called directly.
| #[cfg(any(not(kani), kani_slow))] // this test takes too much memory for our CI | ||
| // environment |
There was a problem hiding this comment.
Yeah it was something like 16Gb, IIRC
Description of changes:
In #1790, @Mark-Simulacrum had some concerns about the code from #1787. This PR aims to address those separately.
Call-outs:
There were a few violations of stacked borrows in the cmsg module. Unfortunately, they aren't completely solvable, as some of them come from the
libccrate. I've modified the code to use our own cmsg implementation, which actually simplifies things a bit.Testing:
I've added MIRI tests for the
s2n-quic-platformcrate to ensure we don't violate the stacked borrows memory model. I've also added a few Kani tests to increase some confidence in the new cmsg code.By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 license.