Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Is something bugging you?

antithesis.com

Post reply on HN
Print view View original

81–90 of 438 posts

Re: Is something bugging you?

#81

Post by samsquire »

__MatrixMan__ wrote: post #78
samsquire wrote: post #56

This is really exciting. I am an absolute beginner at TLA+ but I really like this possible design space. I have an idea for a package manager that combines type system with this style of deterministic testing and state space exploration. Imagine knowing that your invocation of package-manager install Will always work because file system and OS state are part of the deterministic model. or an next gen Helm with type s…

Coincidence, I'm reading this and thinking about test harnesses for my package manager idea, which is really just a thin wrapper around nix, designed under the assumption that the network might partition at any moment: keep the data nearest where it's needed, refer by hash not by name, gossip metadata necessary to find the hash for you, no single points of failure. Tell me more about yours?

I am thinking about state machine progressions and TLA+ style specifications which are invariants over a progression of variables.

Your package manager knows your operating system's current state and the state space of all the control flow graph through the program and configuration together can go to, it can verify that everything lines up and there will be no error when executed a bit like a compiler but without causing the Halting problem.

In TLA+ you can dump a state graph as a dot file, which I turn into a SVG and run with TLA+ graph visualiser.

Types verify possible control flow is valid at every point. We just need to add types to the operating system and file system and represent state space for deterministic verification.

You could hide packages that won't work.

The package manager would have to lookup precached state spaces or download them as part of the verification process.

Re: Is something bugging you?

#82

Post by shermantanktop »

I kept cringing when I read the words “no bugs.”

This is hubris in the classic style - it’s asking for a literal thunderbolt from the heavens.

It may be true, but…come on.

Everyone who has ever written a program has thought they were done only to find one more bug. It’s the fundamental experience of programming to asymptotically approach zero bugs but never actually get there.

Again, perhaps the claim is true but it goes against my instincts to entertain the possibility.

Re: Is something bugging you?

#83

Post by tranceylc »

Invictus0 wrote: post #71

Talk about bad writing. If I don't know what the hell your thing is in the first paragraph, I'm not going to read your whole blog post to find out. Homepage is just as bad.

The article is more of a history lesson and context than it is an ad. I see what you mean, but clicking “product -> What Is Antithesis?” Shows a clear description of what it does. Perhaps that could also either be added to the article or the home page?

Re: Is something bugging you?

#84

Post by sackfield »

"At FoundationDB, once we hit the point of having ~zero bugs and confidence that any new ones would be found immediately, we entered into this blessed condition and we flew. Programming in this state is like living life surrounded by a force field that protects you from all harm. Suddenly, you feel like you can take risks"

When this state hits it really is a thing to behold. Its very empowering to trust your system to this extent, and to know if you introduce a bug a test will save you.

Re: Is something bugging you?

#85

Post by dkyc »

On mobile, the "Let's talk" button in the top right corner is cut off by the carousel menu overlay. Seems like CSS is still out of scope of the bug fixing magic for now.

On a more serious note, it's an interesting blog post, but it comes off as veeery confident about what is clearly an incredibly broad and complex topic. Curious to see how it will work in production.

Re: Is something bugging you?

#86

Post by nlavezzo »

agumonkey wrote: post #80

interesting, this kind of responsive environment is dear but rare i can't recall the last time i went to a place and people even considered investing in such setups i assume that except for hard problems and teams seeking challenges, most people will revert to the mean and refuse any kind of infrastructure work because it's mentally more comfortable piling features and fixing bugs later ps: i wish there was a meetup…

We'll be starting some meetups, attending conferences, etc. this year. Also hop into our Discord if you want to chat, lots of us are in there regularly. discord.gg/antithesis

Re: Is something bugging you?

#87

Post by indiv0 »

michael_j_ward wrote: post #38
indiv0 wrote: post #10

I've been super interested in this field since finding out about it from the `sled` simulation guide [0] (which outlines how FoundationDB does what they do). Currently bringing a similar kind of testing in to our workplace by writing our services to run on top of `madsim` [1]. This lets us continue writing async/await-style services in tokio but then (in tests) replace them with a deterministic executor that patches…

> Dealing with every possible source of non-determinism, re-writing services to be testable/sans-IO [2], etc. takes a lot of engineering effort. Are there public examples of what such a re-write looks like? Also, are you working at a rust shop that's developing this way? Final Note, TigerBeetle is another product that was written this way.

Sure! I mentioned a few orthogonal concepts that go well together, and each of the following examples has a different combination that they employ:

- the company that developed Madsim (RisingWave) [0] [1] is tries hardest to eliminate non-determinism with the broadest scope (stubbing out syscalls, etc.)

- sled [2] itself has an interesting combo of deterministic tests combined with quickcheck+failpoints test case auto-discovery

- Dropbox [3] uses a similar approach but they talk about it a bit more abstractly.

Sans-IO is more documented in Python [4], but str0m [5] and quinn-proto [6] are the best examples in Rust I’m aware of. Note that sans-IO is orthogonal to deterministic test frameworks, but it composes well with them.

With the disclaimer that anything I comment on this site is my opinion alone, and does not reflect the company I work at —— I do work at a rust shop that has utilized these techniques on some projects.

TigerBeetle is an amazing example and I’ve looked at it before! They are really the best example of this approach outside of FoundationDB I think.

[0]: https://risingwave.com/blog/deterministic-simulation-a-new-e...

[1]: https://risingwave.com/blog/applying-deterministic-simulatio...

[2]: https://dropbox.tech/infrastructure/-testing-our-new-sync-en...

[3]: https://github.com/spacejam/sled

[4]: https://fractalideas.com/blog/sans-io-when-rubber-meets-road...

[5]: https://github.com/algesten/str0m

[6]: https://docs.rs/quinn-proto/0.10.6/quinn_proto/struct.Connec...

Re: Is something bugging you?

#88

Post by Aeolun »

foobarqux wrote: post #73
kretaceous wrote: post #22

This might be the best introduction post I've read. Lays the foundation (get it?) for who the people are and what they've built. Then explains how the current thing they are building is a result of the previous thing. It feels that they actually want this problem solved for everyone because they have experienced how good the solution feels. Then tells us about the teams (pretty big names with complex systems) that ha…

Except it doesn't actually explain in what it does: Is it fuzzing? Do you supply your own test cases? Is it testing hardware non-determinism?

Yeah. I could figure out the global idea, but then the mechanics of how it would actually work were very sparse.

Re: Is something bugging you?

#89

Post by krisoft »

candiddevmike wrote: post #61
jwr wrote: post #53

FoundationDB is an impressive achievement, quite possibly the only distributed database out there that lives up to its strict serializability claims (see https://jepsen.io/consistency/models/strict-serializable for a good definition). The way they wrote it is indeed very interesting and a tool that does this for other systems is immediately worth looking at.

> quite possibly the only distributed database out there that lives up to its strict serializability claims Jepsen has never tested FoundationDB, not sure why you claim this and link to Jepsen's site.

> not sure why you claim this and link to Jepsen's site.

They link to the website for a definition of the term they are using.

Re: Is something bugging you?

#90

Post by ComputerGuru »

laiysb wrote: post #64
ComputerGuru wrote: post #41

I was mentally hijacked into clicking the jobs link (despite recently deciding I wasn’t going to go down that rabbit hole again!) but fortunately/unfortunately it is in-person and daily so, so flying out from Chicago a week out of the month won’t work and I don’t even have to ask! More to the point of the story (though I do think the actual point was indeed a hiring or contracting pitch), this reminds me a lot of the…

> I was mentally hijacked into clicking the jobs link (despite recently deciding I wasn’t going to go down that rabbit hole again!) but fortunately/unfortunately it is in-person and daily so, so flying out from Chicago a week out of the month won’t work and I don’t even have to ask! given their PLTR connection, probably not

Oh, suddenly I'm not interested, either! Thanks!
Post reply on HN