41–50 of 52 posts
I've changed my behavior to reflect the incentives but remain sad about it.
Earlier quoted context omitted.
Problem with TLA+ is that it is a completely unrelated tool to the actual programming, and even when everything is done correctly, it doesn't prevent further code changes breaking the model, unless there are work processes in place to update the related model, revalidate it, and only then push the changes into production. As mentioned previously, I think the only tools that are really valuable should be able to produ…
The point of TLA+ is to act as a simple "toy model" for the actual system where you can still figure out relevant failure modes by automated means. Real-world code is a lot more complex so "end to end" proofs, while viable in a sense (static type checking is a kind of proof about the code) have very different and more modest goals than something like TLA+.
[1] https://www.amazon.science/publications/using-lightweight-fo...
imho, model checker suits for the problem with many different states and complex state transformation. But in this case, it's a simple toctou problem.. Using model checker sounds weird for me
If you added model checking to it you could have prevented it though, because people that know how to program a model checking program, will see the error right away.
Earlier quoted context omitted.
Yeah... it has felt kind of ridiculous over the years how many times I have tracked some but I was experiencing down to a timeout someone added in the code for a project I was working with, and I have come to the conclusion over the years that the fix is always to remove the timeout: the existence of a timeout is, inherently, a bug, not a feature, and if your design fundamentally relies on a timeout to function, then…
How would you handle the case when some web service is making calls to a 3rd-party and that 3rd-party is failing in unexpected ways (i.e. under high load or IPs are not answering due to routing issues) to avoid a snowball effect on your service without using the timeout concept in any way?
I'm a fan of more formal methods in progam analysis, but this particular excercise is very hindsight-is-20/20 > In this case, we can set up an invariant stating that the DNS should never be deleted once a newer plan has been applied If that invariant had been expressed in the original code — as I'm sure it now is — it wouldn't have broken in the first place. The invariant is obvious in hindsight, but it's hardly axio…
While one can and will add invariants, as they are discovered, they cannot all be found.
Entscheidungsproblem and Trakhtenbrot's theorem apply here, counterintuitively that the validity of finite models is in co-re but not in re.
Validity in this case is not dependent by the truth of the premise or the truth of the conclusion.
Basically we have to use tools like systems thinking to construct robust systems, we cannot universally use formal methods across frames.
It is one way race conditions are complex.
Hindsight bias makes it seem easy but that is because that is in the co-re side.
Well intended actions with hindsight can often result in brittle systems as their composition tends to set systems in stone, with the belief that axioms are the end solution.
The fact that Gödels completeness theorem may not apply for finite systems when it works so well for infinite ones is hard for me to remember.
Remembering that axiomatization is a powerful tool but not a silver bullet has actually helped me more than I can count.
[0] http://jmc.stanford.edu/articles/circumscription/circumscrip...
Earlier quoted context omitted.
Yeah... it has felt kind of ridiculous over the years how many times I have tracked some but I was experiencing down to a timeout someone added in the code for a project I was working with, and I have come to the conclusion over the years that the fix is always to remove the timeout: the existence of a timeout is, inherently, a bug, not a feature, and if your design fundamentally relies on a timeout to function, then…
How would you handle the case when some web service is making calls to a 3rd-party and that 3rd-party is failing in unexpected ways (i.e. under high load or IPs are not answering due to routing issues) to avoid a snowball effect on your service without using the timeout concept in any way?
Earlier quoted context omitted.
How would you handle the case when some web service is making calls to a 3rd-party and that 3rd-party is failing in unexpected ways (i.e. under high load or IPs are not answering due to routing issues) to avoid a snowball effect on your service without using the timeout concept in any way?
You put the timeout on the socket, not your application. Your application shouldn't care how long it takes, as long as progress is being made, which the socket will know about, but you won't. If you put a timeout on your application and then retry, you'll just make the problem worse. Your original packets are still in a buffer somewhere and still will be processed. Retrying won't help the situation.
Earlier quoted context omitted.
You put the timeout on the socket, not your application. Your application shouldn't care how long it takes, as long as progress is being made, which the socket will know about, but you won't. If you put a timeout on your application and then retry, you'll just make the problem worse. Your original packets are still in a buffer somewhere and still will be processed. Retrying won't help the situation.
The socket should also not have a timeout.
Earlier quoted context omitted.
The socket should also not have a timeout.
Sockets actually need a timeout because there is no signal that a client has disconnected. Eventually, maybe, a router along the path will be nice enough to send you a RST packet, but it isn’t guaranteed.
An incoming one might could have a timeout if there is no other way to garbage collect the connection, but, if at all possible, that should usually be in the higher layers, not the lower ones.
(Maybe read my other response to the person you responded to? I purposefully gave you a really short and matter-of-fact statement that fit into the discussion from the thread more broadly.)
Earlier quoted context omitted.
Sockets actually need a timeout because there is no signal that a client has disconnected. Eventually, maybe, a router along the path will be nice enough to send you a RST packet, but it isn’t guaranteed.
People put a lot of timeouts in code when there are humans in the loop that should handle the timeout. An outgoing socket (as is the case in this scenario) really should not have a timeout. An incoming one might could have a timeout if there is no other way to garbage collect the connection, but, if at all possible, that should usually be in the higher layers, not the lower ones. (Maybe read my other response to the…
A timeout on sockets isn’t negotiable.