News for hackers. Stuff that matters.
Re:Translation of the Rust's core and alloc crates to Coq fo... by couchand on Wednesday May 15, 2024 @09:11AM (#40366456)
On the one hand, we like to encourage learning here. On the other, we prefer not to copy-paste a bunch of possibly-irrelevant content. Well, forgive me for pasting in a StackOverflow answer that may be relevant here: https://stackoverflow.com/questions/11276259/are-data-races-...

> Are "data races" and "race condition" actually the same thing in context of concurrent programming

> No, they are not the same thing. They are not a subset of one another. They are also neither the necessary, nor the sufficient condition for one another.

The really curious thing here is that the Nomicon page also describes this distinction in great detail.

Re:Translation of the Rust's core and alloc crates to Coq fo... by hu3 on Wednesday May 15, 2024 @09:56AM (#40367011)
Ahh the uncalled for snark. A trademark of the Rust community.

I knew of the distinction. Posted anyway for clarity.

So races can still happen. Just not a subset of them.

And as per another responder, smaller subset than it looks at first glance. Even in data races.

And who's we?

-----

original msg I replied to:

> On the one hand, we like to encourage learning here. On the other, we prefer not to copy-paste a bunch of possibly-irrelevant content. Well, forgive me for pasting in a StackOverflow answer that may be relevant here: https://stackoverflow.com/questions/11276259/are-data-races-...

> Are "data races" and "race condition" actually the same thing in context of concurrent programming

> No, they are not the same thing. They are not a subset of one another. They are also neither the necessary, nor the sufficient condition for one another.

The really curious thing here is that the Nomicon page also describes this distinction in great detail.

Re:Translation of the Rust's core and alloc crates to Coq fo... by couchand on Wednesday May 15, 2024 @11:18AM (#40368096)
I apologize if my comment came off as snark. Your comment was nothing but pasted text which ommitted relevant detail, so it was not clear what the intent was. In context, to me, it did not seem to be illuminating. It actually seemed to be introducing confusion where there previously was none.

Data races are not possible in safe Rust. Race conditions are. The distinction is made clear in the Nomicon article, but commenters here are really muddying the waters...

Re:Translation of the Rust's core and alloc crates to Coq fo... by hu3 on Wednesday May 15, 2024 @02:48PM (#40370823)
Clearly there is still confusion since we don't agree (as does other the aforementioned poster).

I could have also belittled your comment as "bunch of possibly-irrelevant content" since most of the content was and still is unnecessary snark.

But then it would have said more about my own etiquette and capability to debate objectively than about the topic at hand.

Our definition of data race seems to differ, and because you don't seem to be able to separate objective discussion from personal attacks, I'll stop here.

Re:Translation of the Rust's core and alloc crates to Coq fo... by tialaramex on Wednesday May 15, 2024 @03:25PM (#40371243)
> I could have also belittled your comment as "bunch of possibly-irrelevant content"

That doesn't really make sense because there are other witnesses, so everybody who knows about this topic can see immediately that you're wrong and the other person is right.

Re:Translation of the Rust's core and alloc crates to Coq fo... by hu3 on Wednesday May 15, 2024 @04:04PM (#40371698)
Regardless if technically right or not tialaramex, couchand's messages also contained belittling and snarky content.

So one could have written just the same about what they wrote because of what it also contained. "bunch of possibly-irrelevant content".

This kind of behavior is not justifiable on technical merits alone. At least it shouldn't be.