placeholder

How MutexGuard was Sync When It Should Not Have Been

A couple of weeks ago, our ongoing effort to formalize Rust’s type system lead to us actually discovering a bug in the Rust standard library: MutexGuard implemented Sync in cases where it s...

Click to view the original at ralfj.de

Hasnain says:

"So all’s well that ends well? Not really. Notice how the bug is not caused by an incorrect piece of code somewhere in the implementation of Mutex. One could go over that entire file, and prove every single line of it correct, and all proofs would go through. The bug is in a line of code that was not written. I don’t think it is very surprising that this was overlooked."

Posted on 2017-06-13T07:08:10+0000