This article is pretty great (both in depth and with a fun twist you can kinda see coming), and the article it cites, “Data Race Patterns in Go” is pretty great, too! https://www.uber.com/blog/data-race-patterns-in-go/
Invariants are essential to large scale programming, because it is impossible to hold the entire state of a system in your head at once. Invariants allow you to focus only on the parts of the code responsible for upholding that invariant, and to just assume it holds elsewhere, thus reducing the combinatorial explosion of the state space and allowing the development of software larger than trivial toy examples.
Yes. Well, invariants don’t reduce the state space, they just make it manageable.
I’m surprised to see no mention of Swift here. Or any other language with value semantics (Go included - you can have value semantics in Go if you don’t use pointers). If you just don’t allow sharing of variables, you can also avoid aliasing.
Yea. It’s a great language. It’s still early and experimental, but there’s also Val which just takes the value semantics subset of Swift: https://www.val-lang.dev/.
This week I’ve had to dig into exclusive and shared row-level locking in Postgres. It’s been interesting comparing that (in my head at least) to how you get exclusing and shared borrows in Rust. E.g. SELECT * WHERE id=123 FOR SHARE is a bit like getting some kind of shared reference to an element in a hashmap in Rust.
To fix my particular deadlock issue I used FOR NO KEY UPDATE and FOR KEY SHARE so it could get a better understanding of what data was changing when, and allow concurrent updates. I actually wonder whether Rust (and any other languages that take up the aliasing/concurrency correctness approach advocated in this article) need an equivalent of FOR KEY SHARE, which would be a kind of reference where you can’t read or write the value but you do know that it won’t be dropped before you are done with it (we already have exclusive ownership of a row via FOR UPDATE, exclusive reference of a row via FOR NO KEY UPDATE and shared reference via FOR SHARE). This might allow for a few more additional patterns where we are currently fighting/getting around the borrow checker.
I actually wonder whether Rust (and […]) need […] a kind of reference where you can’t read or write the value but you do know that it won’t be dropped before you are done with it
Would it be enough to have a newtype of a shared reference such that the newtype’s owner can’t access the contained reference?
The idea is that this new 3rd kind of reference would allow for a concurrent mutable reference to be also held. You can’t read the item so it doesn’t matter if it mutates, so long as the item can’t be dropped (think of it as a liveness proof for an object). I don’t think you could do that in safe Rust just by hiding the shared reference away in an empty interface or whatever, right?
(I suppose at least some cases could be handled by lifetime annotations relating to the thing you want to prove alive - not sure if we’d want to go beyond simple static cases though? Certainly the database example uses runtime locking).
This article is pretty great (both in depth and with a fun twist you can kinda see coming), and the article it cites, “Data Race Patterns in Go” is pretty great, too! https://www.uber.com/blog/data-race-patterns-in-go/
Seems like an argument for a capability system built into the type system.
The more I think about static analysis of capabilities, the less clear it becomes to me.
Could you point me to any books/papers/examples?
Check out the papers here https://www.ponylang.io/community/
Yes. Well, invariants don’t reduce the state space, they just make it manageable.
I’m surprised to see no mention of Swift here. Or any other language with value semantics (Go included - you can have value semantics in Go if you don’t use pointers). If you just don’t allow sharing of variables, you can also avoid aliasing.
I wish Swift on non-Mac platforms was a thing. I mean, I know it’s a thing but I wish it were a thing.
Yea. It’s a great language. It’s still early and experimental, but there’s also Val which just takes the value semantics subset of Swift: https://www.val-lang.dev/.
This week I’ve had to dig into exclusive and shared row-level locking in Postgres. It’s been interesting comparing that (in my head at least) to how you get exclusing and shared borrows in Rust. E.g.
SELECT * WHERE id=123 FOR SHAREis a bit like getting some kind of shared reference to an element in a hashmap in Rust.To fix my particular deadlock issue I used
FOR NO KEY UPDATEandFOR KEY SHAREso it could get a better understanding of what data was changing when, and allow concurrent updates. I actually wonder whether Rust (and any other languages that take up the aliasing/concurrency correctness approach advocated in this article) need an equivalent ofFOR KEY SHARE, which would be a kind of reference where you can’t read or write the value but you do know that it won’t be dropped before you are done with it (we already have exclusive ownership of a row viaFOR UPDATE, exclusive reference of a row viaFOR NO KEY UPDATEand shared reference viaFOR SHARE). This might allow for a few more additional patterns where we are currently fighting/getting around the borrow checker.Would it be enough to have a newtype of a shared reference such that the newtype’s owner can’t access the contained reference?
The idea is that this new 3rd kind of reference would allow for a concurrent mutable reference to be also held. You can’t read the item so it doesn’t matter if it mutates, so long as the item can’t be dropped (think of it as a liveness proof for an object). I don’t think you could do that in safe Rust just by hiding the shared reference away in an empty interface or whatever, right?
(I suppose at least some cases could be handled by lifetime annotations relating to the thing you want to prove alive - not sure if we’d want to go beyond simple static cases though? Certainly the database example uses runtime locking).
I suppose the thing I’m talking about is the “tag” reference capability in Pony.