3 ms·

Is there even an approach to doing that? Intuition tells me that's a mathematically intractable problem.

rhinoceraptor 7y ago
Yes, just probably not with a language as semantically ambiguous as C. Rust for example has guarantees against data races.
gameswithgo 7y ago
Rust prevents data races at compile time. Note that data races, while a common form of race condition, is not the only kind of race condition, and Rust won't prevent the others.
Ygg2 7y ago
You're right to an extent. I think that because of Halting problems, a number of useful properties computer could tell you about itself are limited, because they boil down to solving Halting problem. However, one way to avoid such a problem was basically settling for less accurate, but still strict subproblems. I.e. Rust doesn't stop all race conditions but solves them for a subset of data races. In other words you reject some valid programs (false positive?) in order to make sure all valid programs are really valid (false negative?).
reirob 7y ago
ATS language. It compiles to C and I believe I have seen even that experimentally some kernel module was developped in it. Here some resources: The Wikipedia page: https://en.wikipedia.org/wiki/ATS_(programming_language) https://en.wikipedia.org/wiki/ATS_(programming_language) "A (Not So Gentle) Introduction To Systems Programming In ATS" by Aditya Siram at the StrangeLoop 2017: https://www.youtube.com/watch?v=zt0OQb1DBko https://www.youtube.com/watch?v=zt0OQb1DBko Introduction to ATS, a series of screen casts: https://www.youtube.com/playlist?list=PL6BIXG1a4elsauhh56i5nryB_4K4GMbFq https://www.youtube.com/playlist?list=PL6BIXG1a4elsauhh56i5n... I do not program in ATS because I am not doing anything that needs to be as efficient, so that I have the luxury to enjoy programming and learning Haskell, in the hope that by the time when I would need to write some super secure and performant program that has to run without interruption, and is used by more users than myself, well, I hope that by that time Haskell will evolve enough to allow me to write such a program. Otherwise I might end up using ATS, though honestly the syntax is so ugly.

Yes, just probably not with a language as semantically ambiguous as C. Rust for example has guarantees against data races.

gameswithgo 7y ago

Rust prevents data races at compile time. Note that data races, while a common form of race condition, is not the only kind of race condition, and Rust won't prevent the others.

Ygg2 7y ago

You're right to an extent. I think that because of Halting problems, a number of useful properties computer could tell you about itself are limited, because they boil down to solving Halting problem. However, one way to avoid such a problem was basically settling for less accurate, but still strict subproblems. I.e. Rust doesn't stop all race conditions but solves them for a subset of data races. In other words you reject some valid programs (false positive?) in order to make sure all valid programs are really valid (false negative?).

reirob 7y ago

ATS language. It compiles to C and I believe I have seen even that experimentally some kernel module was developped in it. Here some resources: The Wikipedia page: https://en.wikipedia.org/wiki/ATS_(programming_language) https://en.wikipedia.org/wiki/ATS_(programming_language) "A (Not So Gentle) Introduction To Systems Programming In ATS" by Aditya Siram at the StrangeLoop 2017: https://www.youtube.com/watch?v=zt0OQb1DBko https://www.youtube.com/watch?v=zt0OQb1DBko Introduction to ATS, a series of screen casts: https://www.youtube.com/playlist?list=PL6BIXG1a4elsauhh56i5nryB_4K4GMbFq https://www.youtube.com/playlist?list=PL6BIXG1a4elsauhh56i5n... I do not program in ATS because I am not doing anything that needs to be as efficient, so that I have the luxury to enjoy programming and learning Haskell, in the hope that by the time when I would need to write some super secure and performant program that has to run without interruption, and is used by more users than myself, well, I hope that by that time Haskell will evolve enough to allow me to write such a program. Otherwise I might end up using ATS, though honestly the syntax is so ugly.