amw-zero

This is why specification is much more important than verification / proof. We are bound by how accurate we make our propositions.

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 knows that this isn't true, so we're curious... why are you writing these things?

This in combination with [pg_query](https://github.com/pganalyze/libpg_query) could allow for writing generic static analyzers.

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.

Do not use the word "verified" here.

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 repeating) * When an economic situation finally occurs, then say: "See. I predicted this."

Congrats, you are now an economist.

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 company has been developing this in stealth mode for the past few years), but it is most certainly _not_ a marketing post. These people developed extremely novel testing techniques for FoundationDB and are now generalizing them to work with any containerized application.

It's a big deal.

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 what Antithesis is doing under the hood to combat that.

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 trigger complex interactions between dependencies that are likely almost never tested.

They should clarify that this is focused on functional logic bugs though, I agree with that.

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 often means that a model of the behavior might be more appropriate to test against, e.g. https://concerningquality.com/model-based-testing/. It would take a bit of design work to get this to play nicely with the Antithesis approach, but it's definitely doable.

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 thousands of test cases.

So it's not that this approach is only useful for critical applications, it's that it's low-cost enough to potentially speed up "regular" business application testing.

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://apple.github.io/foundationdb/testing.html.

So in normal cases this would reek of someone being arrogant / overconfident, but here they really have gotten very close to zero bugs.

Yes it looks like containerization is required: https://antithesis.com/docs/getting_started/setup.html#conta...

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 in doing that has always been the foundations of our machines: non-deterministic CPUs and operating systems. Re-building an entire vertical computing stack is practically impossible, so they just _avoid_ it by building a high-fidelity deterministic simulator.

I do wonder how they are checking for equivalence between the simulator and existing OS's, as that sounds like a non-trivial task. But, even still, I'm really bought in to this idea.

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 many ways of solving the consistency problem, but understanding what consistency and serializability is means that you'll be better educated in coming up with solutions.

Also, I believe that all else being equal, you would want serializability. It simplifies everything. There's a new [financial database under development named TigerBeetle](https://docs.tigerbeetle.com/design/consistency). They chose to implement strict serializability by default because:

> Strict consistency guarantees (at the database level) simplify 1) application logic and 2) error handling farther up the stack.

So the banks of today may have to deal with inconsistency, but that doesn't mean the banks of tomorrow want to.

That’s so true.

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 whenever” wasn’t something that the executives of the company thought was a good idea. So we did try and prevent insufficient funds errors as much as possible.

I personally witnessed several scenarios where the company lost a notable amount of money, (not only rated to concurrency bugs of course) and it’s a pretty bad feeling.

Anyway, I’m legitimately curious to know from people who worked at larger banks perhaps. How is weak transaction isolation not a problem for banks?

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.”

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?

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 extremely important.

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's not communicating enough bits, OR the reader isn't familiar enough with what the bits mean - the semantics of the bits.

If the name is too vague, you have to expand it to send more bits, which can be hard to perfectly capture. If the name is accurate but the reader doesn't understand (as often happens when say reading academic papers), then it's an education issue.

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.

> 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) as if using a ledger alone would get rid of the race conditions caused by the read committed isolation level.

But what you described is manually implementing locking, which requires additional schema and application logic.

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.

Yes exactly. That's the approach taken here. The main downside is that it can require sleeps to properly reproduce race conditions.

Exactly, it's a tricky problem. Implementing all transaction isolation levels in a mock is quite an ambitious endeavor.

This will go down as the most legendary sentence by a legendary computer scientist.

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 heard of Coyote (it's still amazing how many tools are out there). It's good that it operates on the actual code level, but I'm still not sure that would reproduce concurrency non-determinism at the database level.

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 serializable and handling transaction retries.

We can’t measure cognitive load though. Or if we can, no one knows a way to apply that to software projects.