amw-zero

13 ms·

91.
by amw-zero 2y ago
Deterministic execution might be well understood by its proponents, but it's a completely niche technique that practically no one uses in practice. You have this jaded tone like this is something that everyone is doing, and everyone kn
92.
by amw-zero 3y ago
This in combination with [pg_query]( https://github.com/pganalyze/libpg_query ) could allow for writing generic static analyzers.
93.
by amw-zero 3y ago
A language has a paved road, and when you go off of that road you are key with extreme annoyance and friction every step of the way. You’re telling people to just ignore the paved road of Rust, which is bad advice.
94.
by amw-zero 3y ago
Do not use the word "verified" here.
95.
by amw-zero 3y ago
Here's the playbook: * Predict that the good times won't last * When the economy is stable, keep posting that the bad times are around the corner * Repeat until an economic situation occurs (it does not matter how long, just keep
96.
by amw-zero 3y ago
I'm assuming you aren't aware of FoundationDB: https://www.foundationdb.org/files/fdb-paper.pdf Having that context puts the post in a much better perspective. It's definitely an introduction post (the c
97.
by amw-zero 3y ago
Is there more info on how Antithesis solves problem number 2 (large state spaces)? I understand the fuzzing / workload generation part well, but there's so many different state space reduction techniques that I don't know wha
98.
by amw-zero 3y ago
Yes, there are plenty of non-functional logic bugs, e.g. performance issues. I think this starts to drastically hone in on the set of "all" bugs though, especially by doing things like network fault injection by default. This will
99.
by amw-zero 3y ago
There's a lot of assertions that I throw into business applications that would be very useful to test in this way. So I don't think this only applies to testing databases. Also, when properties are difficult to think of, that ofte
100.
by amw-zero 3y ago
This is a false dichotomy though. The proposed approach here has a (theoretically) great cost to value ratio. Spending time on a workload generation process, and adding some asserts to your code is much lower cost than hand-writing tens of
101.
by amw-zero 3y ago
I do think that it was a mistake to use the word "all" and imply that there are absolutely no bugs in FoundationDB. However, FoundationDB is truly known as having advanced the state of the art for testing practices: https:/&
102.
by amw-zero 3y ago
Yes it looks like containerization is required: https://antithesis.com/docs/getting_started/setup.html#conta...
103.
by amw-zero 3y ago
I'm trying to avoid diving into the hype cycle about this immediately - but this sounds like the holy grail right? Use your existing application as-is (assuming it's containerized), and simply check properties on it? The blocker i
104.
by amw-zero 3y ago
I hear what you're saying, the real world is often complex. However, I don't agree that means banking examples aren't useful, because they do lay out the problem that all banks have to consider, one way or another. There are
105.
by amw-zero 3y ago
That’s so true.
106.
by amw-zero 3y ago
Hello, I wrote the post. I don’t claim to be a banking expert, but I did work at a payment processor that handled real money, and we used “select for update” extensively. We also (obviously) used a ledger, but “just let everyone overdraft w
107.
by amw-zero 3y ago
Can you elaborate? Does your bank allow you to overdraft on $50k for example? I think it’s more complicated than “eventual consistency solves all problems.”
108.
by amw-zero 3y ago
So you’re recommending a solution that’s fine for a few concurrent users? What about when you have tens of thousands of concurrent users?
109.
by amw-zero 3y ago
That’s really cool. It reminds me of Meta’s hermit, which intercepts system calls and records them so that they can be replayed back deterministically. Non-determinism is the name of all testing. Anything that we can do to improve it is ext
110.
by amw-zero 3y ago
The mathematical intuition for why naming things is hard is definitely tied to information theory and semantics (linguistics). Names communicate bits of information, and they describe a semantic concept. When a name isn't accurate, it&
111.
by amw-zero 3y ago
Maybe an ATM allows that, because the max you can take out of an ATM is $500 or so. I don’t think you want to let a $500k withdrawal go through optimistically.
112.
by amw-zero 3y ago
> Also, consider storing the transactions that change the balances (credits, debits, etc) in a ledger and calculate the balance. You can avoid the complex update logic and keep your accountants and auditors happy. This was written (to me
113.
by amw-zero 3y ago
How can you store ledger operations without locking on the balance? The race condition still exists - you can't accept a withdrawal if the user doesn't have enough funds.
114.
by amw-zero 3y ago
Yes exactly. That's the approach taken here. The main downside is that it can require sleeps to properly reproduce race conditions.
115.
by amw-zero 3y ago
Exactly, it's a tricky problem. Implementing all transaction isolation levels in a mock is quite an ambitious endeavor.
116.
by amw-zero 3y ago
This will go down as the most legendary sentence by a legendary computer scientist.
117.
by amw-zero 3y ago
The issue is that the race condition exists in the database, not in any application code. So you can either simulate the race, or you need to integration test, and that's outside the scope of TLA+ and model checking. I haven't hea
118.
by amw-zero 3y ago
Probably because it’s more work, and it’s logic that you have to write and get correct. Whereas “for update” pretty much just works. But there are definitely many valid solutions, including just setting the specific transaction to serializa
119.
by amw-zero 3y ago
We can’t measure cognitive load though. Or if we can, no one knows a way to apply that to software projects.
120.
by amw-zero 3y ago
I don't think something that specific exists. There are a very large number of formal methods tools, each with different specialties / domains. For verification with proof assistants, [Software Foundations]( https://soft

More ›