Stream: t-lang/wg-unsafe-code-guidelines

Topic: Out-of-thin-air


RalfJ (Oct 12 2019 at 21:47, on Zulip):

@gnzlbg

 FYI the latest revision 1 of the paper suggests that there is consensus on what the fixed semantics of relaxed ought to look like, but since that's a backward incompatible change that software and hardware vendors might need time to adapt to, it proposes to add a new memory order called load_store instead.

I'll wait until someone formalized load_store then and fixed the bugs that so far were always present when models were suggested that did not come with theorems... ;)

gnzlbg (Oct 12 2019 at 21:53, on Zulip):

That paper says that this happened already in http://plv.mpi-sws.org/scfix/paper.pdf

RalfJ (Oct 12 2019 at 21:55, on Zulip):

my reading of the paper is that the SCfix paper suggested one fix but they are suggesting a variant of that, or so? maybe I misread, I only skimmed it

RalfJ (Oct 12 2019 at 21:55, on Zulip):

and also I think we need an operational model to make any sense out of all of that

gnzlbg (Oct 12 2019 at 21:55, on Zulip):

I haven't read this other paper yet, so I can't tell if the solution proposed there is the same as the one in the iso paper

RalfJ (Oct 12 2019 at 21:56, on Zulip):

I mean, C++11 defines a notion of data race using a graph of the whole program execution while at the same time saying data races are UB, which makes it impossible to even say what the program does when executed!

RalfJ (Oct 12 2019 at 21:56, on Zulip):

this is all awfully broken :(

RalfJ (Oct 12 2019 at 21:57, on Zulip):

this relates to your "clobber" question actually

gnzlbg (Oct 12 2019 at 21:57, on Zulip):

maybe wrong thread?

RalfJ (Oct 12 2019 at 21:58, on Zulip):

not really, this is my "ranting about C++ concurrency" thread ;)

gnzlbg (Oct 12 2019 at 21:58, on Zulip):

ah ok, then go ahead :P

gnzlbg (Oct 12 2019 at 21:59, on Zulip):

my personal rant is that it is impossible to explain the C++ concurrency to anybody, because nobody understands it

RalfJ (Oct 12 2019 at 21:59, on Zulip):

"clobber" isn't the effect the code has, it's the bound on the effect. like, if we have a proper operational spec of everything, we can say that the compiler has to assume that the inline assembly somehow alters the machine state, subject to constraints X, Y, Z. so the answer to your question would be "a inline assembly block could cause a data race (and therefore move the machine to the UB-error state). but it also couldn't, and the compiler has to do something that's correct for any possible action of the inline assembly block.

RalfJ (Oct 12 2019 at 21:59, on Zulip):

this may be vague but if I am sure this can be made precise. I just need to throw some greek at it.

RalfJ (Oct 12 2019 at 22:00, on Zulip):

but with an axiomatic model... you can't do anything like that, I don't think. you're just stuck.

gnzlbg (Oct 12 2019 at 22:00, on Zulip):

"a inline assembly block could cause a data race (and therefore move the machine to the UB-error state). but it also couldn't, and the compiler has to do something that's correct for any possible action of the inline assembly block.

That's not really what I was hoping or thinking

gnzlbg (Oct 12 2019 at 22:01, on Zulip):

I was hoping that clobber means that the inline assembly block could alter the machine state, but only in ways that do not cause an error in the abstract machine

RalfJ (Oct 12 2019 at 22:02, on Zulip):

why not? seems like the natural spec to me: the annotations at the inline assembly block basically form a specification for the operation in there. it's like a Hoare triple. the compiler may assume that that spec is correct, but it may not assume anything else about what that block does.

I just dont know how to explain this to people that haven't done interactive program verification in a Hoare logic...^^

RalfJ (Oct 12 2019 at 22:03, on Zulip):

I was hoping that clobber means that the inline assembly block could alter the machine state, but only in ways that do not cause an error in the abstract machine

well that's what I said. the compiler will always assume that we haven't reached the UB-error state.

RalfJ (Oct 12 2019 at 22:03, on Zulip):

the thing is the compiler can't prove that the inline block doesn't cause a data race

RalfJ (Oct 12 2019 at 22:03, on Zulip):

it also may not assume that it does cause a race

gnzlbg (Oct 12 2019 at 22:04, on Zulip):

so it can assume that it does not ?

RalfJ (Oct 12 2019 at 22:04, on Zulip):

yeah

RalfJ (Oct 12 2019 at 22:04, on Zulip):

its not like inline assembly can make UB legal

gnzlbg (Oct 12 2019 at 22:05, on Zulip):

yeah

gnzlbg (Oct 12 2019 at 22:06, on Zulip):

https://llvm.org/docs/LangRef.html#clobber-constraints

The actual clobber constraint is ~{memory}, which means:

indicates that the assembly writes to arbitrary undeclared memory locations – not only the memory pointed to by a declared indirect output.

So it makes sense to me that this is ok as long as those writes do not cause a race.

RalfJ (Oct 12 2019 at 22:07, on Zulip):

OTOH I doubt they mean arbitrary

RalfJ (Oct 12 2019 at 22:07, on Zulip):

like, memory that never had its address escape?

gnzlbg (Oct 12 2019 at 22:07, on Zulip):

maybe not that arbitrary, but you can get the stack pointer, and do... whatever you want

comex (Oct 12 2019 at 22:08, on Zulip):

but you can't overwrite random variables that never had their address taken

comex (Oct 12 2019 at 22:08, on Zulip):

well, you can, but it would be silly for the compiler to guarantee correct execution in that case

gnzlbg (Oct 12 2019 at 22:08, on Zulip):

even if the write isn't completely arbitrary, the compiler has to assume that the assembly block could write to a location that could cause a race

RalfJ (Oct 12 2019 at 22:08, on Zulip):

this stuff gets really "fun" to specify formally when you think of the assembly block doing some action that disturbs the Rust AM abstraction, like page table manipulation, while other AM threads are running. the assembly has a proof obligation here to not break the abstraction... this becomes very compiler-specific quickly (I guess that's expected)

gnzlbg (Oct 12 2019 at 22:08, on Zulip):

and, e.g., consider that when consider whether memory operations can be re-ordered across an inline assembly block

gnzlbg (Oct 12 2019 at 22:09, on Zulip):

so in a sense, an inline assembly block with a ~{memory} clobber must synchronize

RalfJ (Oct 12 2019 at 22:09, on Zulip):

and, e.g., consider that when consider whether memory operations can be re-ordered across an inline assembly block

the compiler will reorder accesses to unescaped locals around unknown code

comex (Oct 12 2019 at 22:09, on Zulip):

GCC documentation:

comex (Oct 12 2019 at 22:09, on Zulip):

"memory"
The "memory" clobber tells the compiler that the assembly code performs memory reads or writes to items other than those listed in the input and output operands (for example, accessing the memory pointed to by one of the input parameters). To ensure memory contains correct values, GCC may need to flush specific register values to memory before executing the asm. Further, the compiler does not assume that any values read from memory before an asm remain unchanged after that asm; it reloads them as needed. Using the "memory" clobber effectively forms a read/write memory barrier for the compiler.

Note that this clobber does not prevent the processor from doing speculative reads past the asm statement. To prevent that, you need processor-specific fence instructions.

RalfJ (Oct 12 2019 at 22:09, on Zulip):

which can contain inline assembly

comex (Oct 12 2019 at 22:09, on Zulip):

just for reference.

RalfJ (Oct 12 2019 at 22:10, on Zulip):

so inline assembly still may not just get the stack ptr and mess with spilled local variables or so

RalfJ (Oct 12 2019 at 22:10, on Zulip):

that's another aspect of "maintaining the abstraction"

comex (Oct 12 2019 at 22:10, on Zulip):

indeed

RalfJ (Oct 12 2019 at 22:11, on Zulip):

within the AM that relies on allocator non-determinism. so that'll somehow have to be extended far enough down the stack here...

RalfJ (Oct 12 2019 at 22:12, on Zulip):

or maybe "escaped" actually becomes a manifest piece of state in some lower level of the Rust AM -- the version of that AM that assembly interacts with. that might be easier.

RalfJ (Oct 12 2019 at 22:12, on Zulip):

anyway I am rambling and should be sleeping. good night!

Last update: Nov 19 2019 at 18:55UTC