47 ms·

Is something bugging you?

• jewel 3y ago
  This reminds me of Java Pathfinder, but for distributed systems.
• bvivek77 3y ago
  Looks promising!!
• deleted 3y ago
  [deleted]
• loadzero 3y ago
  Sounds a bit like jockey applied to qemu. Very neat indeed. https://www.cs.purdue.edu/homes/xyzhang/spring07/Papers/HPL-2005-46.pdf https://www.cs.purdue.edu/homes/xyzhang/spring07/Papers/HPL-...
  • voidmain 3y ago
    There's indeed a connection between record/replay and deterministic execution, but there's a difference worth mentioning, too. Both can tell you about the past, but only deterministic execution can tell you about alternate histories. And that's very valuable both for bug search (fuzzing works better) and for debugging (see for example the graphs where we show when a bug became likely to occur, seconds before it actually occurred). (Also, you won't be able to usefully record a hypervisor with jockey or rr, because those operate in userspace and the actual execution of guest code does not. You could probably record software cpu execution with qemu, but it would be slow) I'm a co-founder of Antithesis.
    • pfdietz 3y ago
      I assume deterministic execution also lets you do failing test case reduction. I've found this sort of high volume random testing w. test case reduction is just a game changer for compiler testing, where there's much the same effect at quickly flushing out newly introduced bugs. I like the subtle dig at type systems. :)
    • loadzero 3y ago
      I have been down this road a little bit, applying the ideas from jockey to write and ship a deterministic HFT system, so I have some understanding of the difficulties here. We needed that for fault tolerance, so we could have a hot synced standby. We did have to record all inputs (and outputs for sanity checking) though. We did also get a good taste of the debugging superpowers you mention in your blog article. We could pull down a trace from a days trading and replay on our own machines, and skip back and forth in time and find the root cause of anything. It sounds like what you have done is something similar, but with your own (AMD64) virtual machine implementation, making it fully deterministic and replayable, and providing useful and custom hardware impls (networking, clock, etc). That sounds like a lot of hard but also fun work. I am missing something though, in that you are not using it just for lockstep sync or deterministic replays, but you are using it for fuzzing. That is, you are altering the replay somehow to find crashes or assertion failures. Ah, I think perhaps you are running a large number of sims with a different seed (for injecting faults or whatnot) for your VM, and then just recording that seed when something fails.
• Rygian 3y ago
  The writing is really enjoyable. > Programming in this state is like living life surrounded by a force field that protects you from all harm. [...] We deleted all of our dependencies (including Zookeeper) because they had bugs, and wrote our own Paxos implementation in very little time and it _had no bugs_. Being able to make that statement and back it by evidence must be indeed a cool thing.
  • llm_trw 3y ago
    I have proved my code has no bugs according to the spec. I do not make the claim my spec has no bugs.
    • deleted 3y ago
      [deleted]
    • yasuocidal 3y ago
      "Its not a bug, its a feature"
    • coldtea 3y ago
      With formal proof systems, you can also claim that for your spec.
      • svieira 3y ago
        A formal proof is only as good as what-you-are-proving maps to what-you-intended-to-prove.
      • AlotOfReading 3y ago
        I've written formal proofs with bugs more than once. Reality is much messier than you can encode into any proof and there will ultimately be a boundary where the real systems you're trying to build can still have bugs. Formal verification is incredibly, amazingly good if you achieve it, but it's not the same as "perfect".
      • llm_trw 3y ago
• flgstnd 3y ago
  the palantir testimonial on the landing page is funny
  • CiPHPerCoder 3y ago
    Even funnier if you manage to click "Declassify" :)
    • flgstnd 3y ago
      you're ip address is probably in the palantir databases anyway :o
  • bhammerling 3y ago
    [dead]
  • zellyn 3y ago
    And if you highlight the redactions, it reads: REDACTED REDACTED REDACTED REDACTED REDACTED REDACTED and REDACTED REDACTED? REDACTED REDACTED Antithesis REDACTED REDACTED REDACTED REDACTED, REDACTED REDACTED REDACTED REDACTED. REDACTED REDACTED Palantir REDACTED REDACTED REDACTED REDACTED REDACTED REDACTED REDACTED. :-)
  • couchand 3y ago
    This sort of awkward joke made to cover for capitalist illogic makes us all dumber.
• larsiusprime 3y ago
  Was an eaaaaaaaarly tester for this. Pretty neat stuff.
• indiv0 3y ago
  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 all sources of non-determinism (including dependencies that call out to the OS). It's pretty seamless. The author of this article isn't joking when they say that the startup cost of this effort is monumental. Dealing with every possible source of non-determinism, re-writing services to be testable/sans-IO [2], etc. takes a lot of engineering effort. Once the system is in place though, it's hard to describe just how confident you feel in your code. Combined with tools like quickcheck [3], you can test hundreds of thousands of subtle failure cases in I/O, event ordering, timeouts, dropped packets, filesystem failures, etc. This kind of testing is an incredibly powerful tool to have in your toolbelt, if you have the patience and fortitude to invest in it. As for Antithesis itself, it looks very very cool. Bringing the deterministic testing down the stack to below the OS is awesome. Should make it possible to test entire systems without wiring up a harness manually every time. Can’t wait to try it out! [0]: https://sled.rs/simulation.html https://sled.rs/simulation.html [1]: https://github.com/madsim-rs/madsim?tab=readme-ov-file#madsim https://github.com/madsim-rs/madsim?tab=readme-ov-file#madsi... [2]: https://sans-io.readthedocs.io/ https://sans-io.readthedocs.io/ [3]: https://github.com/BurntSushi/quickcheck?tab=readme-ov-file#quickcheck https://github.com/BurntSushi/quickcheck?tab=readme-ov-file#...
  • michael_j_ward 3y ago
    > 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.
    • wwilson 3y ago
      TigerBeetle is actually another customer of ours. You might ask why, given that they have their own, very sophisticated simulation testing. The answer is that they're so fanatical about correctness, they wanted a "red team" for their own fault simulator, in case a bug in their tests might hide a bug in their database! I gotta say, that is some next-level commitment to writing a good database. Disclosure: Antithesis co-founder here.
• pfdietz 3y ago
  This sounds quite cool. Although it doesn't say so, I imagine the name is riff off Hypothesis, the testing tool that performs automatic test case simplification in a general way.
  • intuitionist 3y ago
    (I’m an early employee of what was, on my start date, just called “Void Star.”) As I recall it, the name meant two things: 1. Our “autonomous testing” approach is the opposite, or the antithesis, of flaky and unreliable testing methodologies. 2. You can think of our product as standing in dialectical opposition to buggy customer software, pointing out its internal contradictions (bugs) and together synthesizing a new, bug-free software product. (N.b.: I’ve never actually read Hegel.) We did note the resonance with Hypothesis (a library I like a lot!) at the time, but it was just an added bonus :).
• vinnymac 3y ago
  I wonder if they are working on a time travel debugger. If it is truly deterministic presumably you could visit any point in time after a record is made and replay it.
  • wwilson 3y ago
    No comment. :-) Disclosure: I am a co-founder of Antithesis.
    • bloopernova 3y ago
      It looks amazing, nice work! Do you have any plans to let small open source teams use the project for free? Obviously you have bills to pay and your customers are happy to do that, but I was wondering if you'd allow open source projects access to your service once a week or something. Partly because I want to play with this and I can't see my employer or client paying for it! But also it fits neatly into "DX", the Developer Experience, i.e. making the development cycle as friction free for devs as possible. I'm DevOps with a lifelong interest in UX, so DX is something I'm excited about.
      • wwilson 3y ago
        Pricing suitable for small teams, and perhaps even a free tier, is absolutely on the roadmap. We decided to build the "hard", security-obsessed version of the infrastructure first -- single-tenant, with dedicated and physically isolated hardware and networking for every customer. That means there's a bit of per-customer overhead that we have to recoup. In the future, we will probably have a multi-tenant offering that's easier for open source projects to adopt. In the meantime, if your project is cool and would benefit from our testing, you can try to get our research team interested in using it as part of the curriculum that makes our platform smarter. Disclosure: I'm an Antithesis co-founder.
      • nlavezzo 3y ago
        We've actually done quite a bit of testing on open source projects as we've built this, and have discussed doing an on-going program of testing open source projects that have interested contributors. We'd probably find some interesting things and could do some write-ups. Reach out to us via our contact page or contact@antithesis.com and let's chat.
• chrispy513 3y ago
  This looks to be an incredible tool that was years in the making. Excited to see where it goes from here!
• User23 3y ago
  Reminds me of the clever hack of playing back TCP dump logs from prod on a test network, but dialed up. Neat. Naturally I’d prefer professional programmers learn the cognitive tools for manageably reasoning about nondeterminism, but they’ve been around over half a century and it hasn’t happened yet. What’s really interesting to me is that the simulation adequately replicates the real network. One of the more popular criticisms of analytical approaches is sone variant of: yeah, but the real network isn’t going to behave like your model. Which by the way is an entirely plausible concern for anyone who has messed with that layer.
  • Rygian 3y ago
    What is interesting here is that the solution could fuzz-test anything, including the network model, leading to failures even more implausible than reality.
  • zamfi 3y ago
    > Naturally I’d prefer professional programmers learn the cognitive tools for manageably reasoning about nondeterminism It’s not an either-or here, though. Part of the challenge is you’re not always thinking about all the non-determinisms in your code, and the interconnections between your code and other code (whose behavior you can sometimes only assume) can make that close to impossible. Part of that is the “your model of the network” critique, but also part of that is “your model of how people will use your software” isn’t necessarily correct either.
• deleted 3y ago
  [deleted]
• kretaceous 3y ago
  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 have already used it. All of these wrapped in good writing that appeals to developers/founders. Landing page is great too!
  • getoffmycase 3y ago
    The entire testing system they describe feels like something I can strive towards too. They make you want their solution because it offers a way of life and thinking and doing like you've never experienced before
  • foobarqux 3y ago
    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?
    • Aeolun 3y ago
      Yeah. I could figure out the global idea, but then the mechanics of how it would actually work were very sparse.
    • wwilson 3y ago
      Post author here. Sorry it was vague, but there's only so much detail you can go into in a blog post aimed at general audiences. Our documentation (https://antithesis.com/docs/ https://antithesis.com/docs/) has a lot more info. Here's my attempt at a more complete answer: think of the story of the blind men and the elephant. There's a thing, called fuzzing, invented by security researchers. There's a thing, called property-based testing, invented by functional programmers. There's a thing, called network simulation, invented by distributed systems people. There's a thing, called rare-event simulation, invented by physicists (!). But if you squint, all of these things are really the same kind of thing, which we call "autonomous testing". It's where you express high-level properties of your system, and have the computer do the grunt work to see if they're true. Antithesis is our attempt to take the best ideas from each of these fields, and turn them into something really usable for the vast majority of software. We believe the two fundamental problems preventing widespread adoption of autonomous testing are: (1) most software is non-deterministic, but non-determinism breaks the core feedback loop that guides things like coverage-guided fuzzing. (2) the state space you're searching is inconceivably vast, and the search problem in full generality is insolubly hard. Antithesis tries to address both of these problems. So... is it fuzzing? Sort of, except you can apply it to whole interacting networked systems, not just standalone parsers and libraries. Is it property-based testing? Sort of, except you can express properties that require a "global" view of the entire state space traversed by the system, which could never be locally asserted in code. Is it fault injection or chaos testing? Sort of, except that it can use the techniques of coverage guided fuzzing to get deep into the nooks and crannies of your software, and determinism to ensure that every bug is replayable, no matter how weird it is. It's hard to explain, because it's hard to wrap your arms around the whole thing. But our other big goal is to make all of this easy to understand and easy to use. In some ways, that's proved to be even harder than the very hard technological problems we've faced. But we're excited and up for it, and we think the payoff could be big for our whole industry. Your feedback about what's explained well and what's explained poorly is an important signal for us in this third very hard task. Please keep giving it to us!
• sneak 3y ago
  Imagine being proud of working for Palantir.
  • mgfist 3y ago
    Your life depends on lots of unsavory tasks.
    • sneak 3y ago
      Yes, like sewage pipe maintenance. Not data mining to figure out who to assassinate without trial. Using the “unsavory” euphemism for unethical and illegal violence is somewhat of a deception, is it not?
      • mgfist 3y ago
        No, I did mean to say potentially "unethical" tasks. Much of national defense is deemed "unethical" by many, yet a critical function that allows you to live a peaceful life.
• jitl 3y ago
  To me this is very reminiscent of time travel debugging tools like the one used for Firefox’s C++ code, rr / Pernosco: https://pernos.co/ https://pernos.co/
  • rvnx 3y ago
    Seems more like a fuzzer for Docker images. Like this: https://docs.gitlab.com/ee/user/application_security/coverage_fuzzing/ https://docs.gitlab.com/ee/user/application_security/coverag... It won't tell you whether the software works correctly, it will just tell you if it raises an exception or crashes. Put a fuzzer on Chrome for example, you won't catch most of the issues it has, though Chrome actually has tons of bugs and issues, but you may find security issues if you devote a big enough budget to run your fuzzer long time enough to cover all the branches. So it's good in the case where you use "exceptions as tests", where any minor out-of-scope behavior raises an exception and all the cases are pre-planned (a bit like you baked-in runtime checks, and the fuzzer explores them)
    • jitl 3y ago
      The similarity is about obtaining determinism through something like a hypervisor. The way rr works is it basically writes down the result of all the system calls, etc, basically everything that ended up on the Turing machine’s tape, so you can rewind and replay.
  • icholy 3y ago
    I was really hoping this would be rr but more general purpose.
• intrasight 3y ago
  >It’s pretty weird for a startup to remain in stealth for over five years. Not really. I have friends who work for a startup that's been in "stealth" for 20 years. Stealth is a business model not a phase.
• jimbokun 3y ago
  > The biggest effect was that it gave our tiny engineering team the productivity of a team 50x its size. I feel like the idea of the legendary "10x" developer has been bastardized to just mean workers who work 15 hours a day 6.5 days a week to get something out the door until they burn out. But here's your real 10x (or 50x) productivity. People who implement something very few people even considered or understood to be possible, which then gives amazing leverage to deliver working software in a fraction of the time.
  • FirmwareBurner 3y ago
    Your definition is also vague. Someone still needs to do the legwork. One man armies who can do everything themselves don't really fit in standardized teams where everything is compartmentalized and work divided and spread out. They work best on their own projects with nobody else in their way, no colleagues, no managers, but that's not most jobs. Once you're part of a team, you can't do too much work yourself no matter how good you are, as inevitably the other slower/weaker team members will slow you down as you'll fight dealing with the issues they introduce into the project or the issues from management, so every team moves at the speed of the lowest common denominator no matter their rockstars.
    • jollyllama 3y ago
      That rings true and is probably why the 10x engineers I have seen usually work on devops or modify the framework the other devs are using in some way. For example, an engineer who speeds up a build or test suite by an order of magnitude is easily a 10x engineer in most organizations, in terms of man hours saved.
      • FirmwareBurner 3y ago
        > For example, an engineer who speeds up a build or test suite by an order of magnitude is easily a 10x engineer in most organizations, in terms of man hours saved. Yeah but this isn't something scalable that can happen regularly as part of your job description. Like most jobs/companies don't have so many low hanging fruits to pick that someone can speed of build by orders of magnitude on a weekly basis. It's usually a one time thing. And one time things don't usually make you a 10x dev. Maybe you just got lucky once to see something others missed. And often times at big places most people know where the low hanging fruits are and can fix them, but management, release schedules and tech debt are perpetually in the way. IMHO what makes you a 10x dev is you always know how to unblock people no matter the issue so that the project is constantly smooth saling, not chasing orders of magnitude improvements unicorns.
• agentultra 3y ago
  I got similar productivity boosts after learning TLA+ and Alloy. Simulation is an interesting approach but I am curious if they ever implemented the simulation wrong would it report errors that don't happen on the target platform or fail to find errors that the target platform reports? How wide the gap is will matter... and how many possible platforms and configurations will the hypervisor cover?
• ComputerGuru 3y ago
  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 internal tests the SQLite team has. I would love to hear from someone with access to those if they feel the same way.
  • laiysb 3y ago
    > 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
    • ComputerGuru 3y ago
      Oh, suddenly I'm not interested, either! Thanks!
• timwis 3y ago
  Gosh, I know it's a bit late, but I wish they'd called the product _The Prime Radiant_ Fans of Asimov's _Foundation_ series will appreciate the analogue to how this system aims to predict every eventuality based on every possible combination of events, a la psychohistory. P.S. amazing intro post. Can't wait to try the product.
  • rvnx 3y ago
    It would be the opposite of the product: For a software not interacting with the real world, there is only one possibility for frame N+1, if you know the state of a system. https://en.wikipedia.org/wiki/Determinism https://en.wikipedia.org/wiki/Determinism PRNG are illusions, just misunderstood by humans.
    • samatman 3y ago
      Did you intend to link to https://en.wikipedia.org/wiki/Deterministic_algorithm https://en.wikipedia.org/wiki/Deterministic_algorithm?
      • rvnx 3y ago
        No, it is a reference to https://en.wikipedia.org/wiki/Laplace%27s_demon https://en.wikipedia.org/wiki/Laplace%27s_demon - Pierre Simon Laplace, A Philosophical Essay on Probabilities (if you know the state of a system + all the rules then you can know the next state) and determinism actually applies way beyond just algorithms.
    • timwis 3y ago
      Feels like I may have brought a spoon to a gun fight, but I would have considered psychohistory to be the ultimate extrapolation of determinism, and the fact that the prime radiant is able to predict _which_ version of events will happen is because it (somehow) knows the state of the system. Of course, to argue against myself, it would surely be based on layers of probabilities, and they say several times in the series that it can't predict low-level specific things, just high-level things. And perhaps the whole underlying question posed by the series is whether the universe really is deterministic. But anyway I don't think it's all off-base.
• 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 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.
  • wilkystyle 3y ago
    Does it even need to be containerized? According to the post, it sounds like Antithesis is a solution at the hypervisor layer.
    • amw-zero 3y ago
      Yes it looks like containerization is required: https://antithesis.com/docs/getting_started/setup.html#containerize-your-software https://antithesis.com/docs/getting_started/setup.html#conta...
      • voidmain 3y ago
        Containers are doing two jobs for us: they give our customers a convenient way to send us software to run, and they give us a convenient place to simulate the network boundary between different machines in a distributed system. The whole guest operating system running the containers is also running inside the deterministic hypervisor and under test (and it's mostly just NixOS Linux, not something weird that we wrote). I'm a co-founder of Antithesis.
        • tikhonj 3y ago
          Oh, cool to hear you're using NixOS. The Nix philosophy totally gels with the philosophy described in the post. But it's also probably fair to describe NixOS as something weird that somebody else wrote :)
• xyzelement 3y ago
  I appreciated this post. Separately from what they are talking about, I found this bit insightful: // This limits the value of testing, because if you had the foresight to write a test for a particular case, then you probably had the foresight to make the code handle that case too. I often felt this way when I saw developers feel a sense of doing good work and creating safe software because they wrote unit tests like expect add(2,2) = 4. There is basically a 1-1 correlation between cases you thought to test and that you coded for, which is really no better off in terms of unexplored scenarios. I get that this has some incremental value in catching blatant miscoding and regressions down the road so it's helpful, it's just not getting at the main thing that will kill you. I felt similarly about human QA back in my finance days that asked developers for a test plan. If the dev writes a test plan, it also only covers what the dev already thought about. So I asked my team to write the vaguest/highest level test plan possible (eg, "it should now be possible to trade a Singaporean bond" rather than "type the Singaporean bond ticker into the field, type the amount, type the yield, click buy or sell") - the vagueness made more room for the QA person to do something different (even things like tabbing vs clicking, or filling the fields out of sequence, or misreading the labels) than how the dev saw it, which is the whole point.
• jwr 3y ago
  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 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.
  • candiddevmike 3y ago
    > 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.
    • nlavezzo 3y ago
      FDB co-founder here. Aphyr / Jepsen never tested FDB because, as he tweeted "their testing appears to be waaaay more rigorous than mine." We actually put a screen cap of that tweet in the blog post linked here.
      • eevmanu 3y ago
        Just a heads-up for anyone diving deeper into this thread - I dug into the original tweet and managed to track down the parent tweet right here: [1]. Moreover, there's a snapshot on archive.org [2] capturing the reply along with the quote in question. Interestingly, there's also a snapshot from foundationdb.com [3] that discusses the outcomes of running Jepsen tests on FDB. Worth checking out for those interested in the technical nitty-gritty. [1]: https://twitter.com/obfuscurity/status/405016890306985984 https://twitter.com/obfuscurity/status/405016890306985984 [2]: https://web.archive.org/web/20220805112242/https://twitter.com/obfuscurity/status/405016890306985984 https://web.archive.org/web/20220805112242/https://twitter.c... [3]: https://web.archive.org/web/20150325003526/http://blog.foundationdb.com/call-me-maybe-foundationdb-vs-jepsen https://web.archive.org/web/20150325003526/http://blog.found...
    • krisoft 3y ago
• aduffy 3y ago
  Looks like this coincides with seed funding[1], congrats folks! Did you guys just bootstrap through the last 5 years of development? [1] https://www.saltwire.com/cape-breton/business/code-testing-startup-antithesis-raises-seed-funding-at-215-million-valuation-100938096/ https://www.saltwire.com/cape-breton/business/code-testing-s...
• samsquire 3y ago
  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 <tool name> Will always work because file system and OS state are part of the deterministic model. or an next gen Helm with type system and state space exploration is tested: kubectl apply <yaml> will always work when it comes up because all configuration state space exploration has been tested thanks to types.
  • __MatrixMan__ 3y ago
    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?
    • samsquire 3y ago
      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.
• traspler 3y ago
  Checking their bug report which should contain "detailed information about a particular bug" I am not sure I can fully understand those claims: https://public.antithesis.com/report/ZsfkRkU58VYYW1yRVF8zsvUz/MX3yyG71sJvDM8cVzXljvRGAmjQLb9weaaqkELjaQRI.html https://public.antithesis.com/report/ZsfkRkU58VYYW1yRVF8zsvU... To my untrained eye I get: Logs, a graph of when in time the bug happened over multiple runs and a statistical analysis which part of the application code could be invovled. The statistical analysis is nice but it is completely flat, without any hierarchical relationships making it quite hard to parse mentally. I kind of expected more context to be provided about inputs, steps and systems that lead to the bug. Is it expected to then start adding all the logging/debugging that might be missing from the logs and re-run it to track it down? I hoped that given the deterministic systems and inputs there could be more initial hints provided.
• Invictus0 3y ago
  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.
  • tranceylc 3y ago
    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?
  • terpimost 3y ago
    Could you give example of a good writing according to your perspective?
• agumonkey 3y ago
  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 of teams like this, or even job boards :)
  • nlavezzo 3y ago
    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
    • agumonkey 3y ago
      oh, that's cool, thanks
• shermantanktop 3y ago
  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.
  • rkangel 3y ago
    I think there is something interesting about the fact that someone writing "no bugs" makes us all uncomfortable. If they really did have a complex product, running in production from a sizeable userbase and had 2 bug reports ever, then I think it's a reasonable thing to say. The fact that it isn't a reasonable thing to say for the most other software is a little sad.
    • shermantanktop 3y ago
      Right, the claim may be true, but I have a visceral reaction to it. And tbh I'd be hesitant to work with someone who made a zero-bugs claim about their own work.
  • sfink 3y ago
    Yeah, same. It suggests that you must be employing one of the time-honored approaches to getting zero bugs: * Redefine all bugs as features * Redefine "bug" to conveniently only apply to the things your system prevents * Don't write software This reminds me of bugzilla's "Zarro Boogs" phrase that pointedly avoids saying "Zero Bugs" because it's such a deceptive term, see https://en.wikipedia.org/wiki/Bugzilla https://en.wikipedia.org/wiki/Bugzilla Being able to say "no bugs" with justifiable confidence, even when restricting it to some class of bugs, is truly a great and significant thing. cf Rust. But claiming to have no bugs is cringeworthy.
  • chinchilla2020 3y ago
    It's a marketing blog post, not a technical post. Something about the whole thing feels icky.
• sackfield 3y ago
  "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.
• dkyc 3y ago
  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.
  • wruza 3y ago
    Yeah, if only there was some scientific way to ensure that elements don't overlap, let's call it "constraints" maybe, so one could test layouts by simply solving, idk... something like a set of linear equations? Hope some day CSS will stop being "aweso"me and become nothing in favor of a useful layout system.
  • wwilson 3y ago
    Aww... crap, you're right. I knew we should have finished the UI testing product and run it on ourselves before launching. Disclosure: Antithesis co-founder.
  • terpimost 3y ago
    Designer here, sorry, it is intentional. I thought horizontally scrollable menu is more straightforward than full screen expander.
• thomastraum 3y ago
  https://antithesis.com/images/people/will.jpg https://antithesis.com/images/people/will.jpg the look of the CEO is selling the software to me automatically. reliable and nice
• islandert 3y ago
  There’s a straightforward way to reach this testing state for optimization problems. Write 2 implementations of the code, one that is simple/slow and one that is optimized. Generate random inputs and assert outputs match correctly. I’ve used this for leetcode-style problems and have never failed on correctness. It is liberating to code in systems that test like this for the exact reasons mentioned in the article.
  • mrkeen 3y ago
    Non-overlapping problem spaces. Leet-code ends in unit-testing land, this product begins in system-testing land.
• Qwuke 3y ago
  I met Antithesis at Strangeloop this year and got to talk to employees about the state of the art of automated fault injection that I was following when I worked at Amazon, and I cannot overstate how their product is a huge leap forward compared to many of the formal verification systems being used today. I actually got to follow their bug tracking process on an issue they identified in Apache Spark streaming - going off of the docs, they managed to identify a subtle and insidious correctness error in a common operation that would've caused headaches in low visibility edge case for years at that point. In the end the docs were incorrect, but after that showing I cannot imagine how critical tools like Antithesis will be inside companies building distributed systems. I hope we get some blog posts that dig into the technical weeds soon, I'd love to hear what brought them to their current approach.
• BoppreH 3y ago
  Three thoughts: 1. It's a brilliant idea that came at the right time. It feels like people are finally losing patience with flaky software, see developer sentiment on: fuzzers, static typing, memory safety, standardized protocols, containers, etc. 2. It's meant to be niche. $2 per hour per CPU (or $7000 per year per CPU if reserved), no free tier for hobby or FOSS, and the only way to try/buy is to contact them. Ouch. It's a valid business model, I'm just sad it's not going for maximum positive impact. 3. Kudos for the high quality writing and documentation, and I absolutely love that the docs include things like (emphasis in original): > If a bug is found in production, or by your customers, you should demand an explanation from us. That's exactly how you buy developer goodwill. Reminds me of Mullvad, who I still recommend to people even after they dropped the ball on me.
  • wwilson 3y ago
    Thanks for your kind words! As I mention in this comment (https://news.ycombinator.com/item?id=39358526 https://news.ycombinator.com/item?id=39358526) we are planning to have pricing suitable for small teams, and perhaps even a free tier for FOSS, in the future. Disclosure: Antithesis co-founder.
    • eatonphil 3y ago
      There a few FOSS projects I'd love to set this up for if you ever get to the free tier. :)
  • jerf 3y ago
    "It's meant to be niche. $2 per hour per CPU (or $7000 per year per CPU if reserved), no free tier for hobby or FOSS, and the only way to try/buy is to contact them. Ouch. It's a valid business model, I'm just sad it's not going for maximum positive impact." This is the sort of thing that, if it takes off, will start affecting the entire software world. Hardware will start adding features to support it. In 30 years this may simply be how computing works. But the pioneers need to recover the costs of the arrows they got stuck with before it can really spread out. Don't look at this an event, but as the beginning of a process.
  • 3y ago
• benrutter 3y ago
  This is a great pitch, and I don't want to come across as negative, but I feel like a statement like "we found all bugs" can only be true with a very narrow definition of bug. The most pernicious, hard-to-find bugs that I've come across have all been around the business logic of an application, rather than it hitting into an error state. I'm thinking of the category where you have something like "a database is currently reporting a completed transaction against a customer, but no completed purchase item, how should it be displayed on the customer recent transactions page?". Implementing something where "a thing will appear and not crash" in those cases is one thing, but making sure that it actually makes sense as a choice given all the context of everyone elses choices everywhere else in the stack is a lot harder. Or to take a database, something along the lines of "our query planner produces a really suboptimal plan in this edge-case". Neither of those types of problems could ever be automatically detected, because they aren't issues of the programming reaching an error state- the issue is figuring out in the first place what "correct" actually is for you application. Maybe I'm setting the bar too high for what a "bug" is, but I guess my point is, its one thing to fantasize about having zero bugs, its another to build software in the real world. I probably still settle for 0 run time errors though to be fair. . .
  • moritonal 3y ago
    Good summary of the hard part of being a software developer that deals with clients.
    • Aachen 3y ago
      What software developer does not deal with clients (and makes a living)?
      • ejb999 3y ago
        lots of software developers never deal with clients (clients as in the people who will actually use the software) - most of them in fact, in any of the big companies I have worked for anyway...and that is probably not a good thing. I myself, prefer to work with the people who will actually use what I build - get a better product hat way.
• aftbit 3y ago
  This "no bugs" maximalism is counterproductive. There are many classes of bugs that this cannot hope to handle. For example, let's say I have a transaction processing application that speaks to Stripe to handle the credit card flow. What happens if Stripe begins send a webhook showing that it rejected my transactions but report them as completed successfully when I poll them? The need to "delete all of our dependencies" (I presume they wrote their own OS kernel too?) in FoundationDB shows that upstream bugs will always sneak through this tooling.
• mempko 3y ago
  In my career I learned two powerful tools to get bug free code. Design by Contract and Randomized testing. I had to roll this by myself for each project I did. Antithesis seems to systematize it and created great tooling around it. That's Great!!! However, looking at their docs they rely on assertion failures to find bugs. I believe Antithesis has a missed opportunity here by not properly pushing for Design by Contract instead of generic use of assertions. They don't even mention Design by Contract. I suspect the vast majority of people here on HN have never heard of it. They should create a Design by Contract SDK for languages that don't have one (think most languages) that interacts nicely with tooling and only fallback to generic assertions when their SDK is not available. A Design by Contract SDK would provide better error messages over generic assertions, further helping users solve bugs. In fact, their testing framework is useless without contracts being diligently used. It requires a different training and mindset from engineers. Teaching them Design by Contract puts them in that frame of mind. They have an opportunity to teach Design by Contract to a new generation of engineers. I'm surprised they don't even mention it.
  • mrkeen 3y ago
    I've never gotten anything more out of DbC than it being assertions and if-statements, but described using fancy English. I even worked with the creator of C4J a few years ago.
    • mempko 3y ago
      The primary benefit imo is * Way of thinking and discipline. Instead of adhock assertions, you deliberately state in code "These are the preconditions, invariants, and postconditions" of this function/module * Better error messages. * Better documentation (can automate extracting the contracts as documentation). * Better tooling. Can automate creating tests from preconditions. You can sample the functions input space and make sure invariants and postconditions hold. It's like, do you name all your functions 'func a1, func a2, func a3' or do you provide better names?
  • darkteflon 3y ago
    What’s your favourite writing on best practices for randomised testing?
• 0xbadcafebee 3y ago
  > The biggest effect was that it gave our tiny engineering team the productivity of a team 50x its size. 49 years ago, a man named Fred Brooks published a book, wherein he postulated that adding people to a late software project makes it later. It's staggering that 49 years later, people are still discovering that having a larger engineering team does not make your work more productive (or better). So what does make work more productive? Productivity requires efficiency. Efficiency is expensive, complicated, nuanced, curt. You can't just start out from day 1 with an efficient team or company. It has to be grown, intentionally, continuously, like a garden of fragile flowers in a harsh environment. Is the soil's pH right? Good. Is it getting enough sun? Good. Wait, is that leaf a little yellow? Might need to shade it. Hmm, are we watering it too much? Let's change some things and see. Ok, doing better now. Ah, it's growing fast now. Let's trim some of those lower leaves. Hmm, it's looking a little tall, is it growing too fast? Maybe it does need more sun after all. If you really pay attention, and continue to make changes towards the goal of efficiency, you'll get there. No need for a 10x developer or 3 billion dollars. You just have to listen, look, change, measure, repeat. Eventually you'll feel the magic of zooming along productively. But you have to keep your eye on it until it blooms. And then keep it blooming...
• Communitivity 3y ago
  There are situations where no bugs is an important requirement, if it means no bugs that cause a noticeable failure. Things such as planes, submarines, nuclear reactors. For those there is provably correct code. That takes a long time to write, and I mean a really long time. Applying that to all software doesn't make sense from a commercial perspective. There are areas where improvements can have a big impact though, such as language safety improvements (Rust) and cybersecurity requirements regarding private data protection. I see those as being the biggest win. I don't see no bugs in a distributed database as important enough to delay shipping for 5 years, but (a) it's not my baby; (b) I don't know what industries/use cases they are targeting. For me it's much more important to ship something with no critical bugs early, get user feedback, iterate, then rinse and repeat continually.
  • 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 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.
  • 0xbadcafebee 3y ago
    A lot of people underestimate the power of QA. Yeah, it would be great if we could just perfectly engineer something out of the gate. But you can also just take several months to stare at something, poke at it, jiggle it, and fix every conceivable problem, before shipping it. Heresy in the software world, but in every other part of the world it's called quality.
  • mrkeen 3y ago
    > I don't see no bugs in a distributed database as important enough to delay shipping for 5 years The marketplace has enough distributed databases with bugs. There's a nice catalogue of them at jepsen.io. > For me it's much more important to ship something with no critical bugs early, get user feedback, iterate, then rinse and repeat continually. * You can't really choose which bugs are critical if you're selling a database. A lost write is as critical as the customer deems it is. * You're not limited to your own users' feedback. There's plenty of users out there who disapprove of a buggy database, so you can probably take their views onboard before release.
• fleaflicker 3y ago
  Business value is a good way to think about it: > As a software developer, fixing bugs is a good thing. Right? Isn’t it always a good thing? > No! > Fixing bugs is only important when the value of having the bug fixed exceeds the cost of the fixing it. https://www.joelonsoftware.com/2001/07/31/hard-assed-bug-fixin/ https://www.joelonsoftware.com/2001/07/31/hard-assed-bug-fix...
  • pfdietz 3y ago
    If you have high volume automated testing, you want to fix all the bugs, even ones not directly affecting customers, otherwise they keep showing up and may keep you from finding other more customer-relevant bugs.
• coolThingsFirst 3y ago
  Why are all the cool people working on DBs and talking about Paxos?
• A-Dmonkey 3y ago
  one of the best applications yet of AI in cyber
• angryguy555 3y ago
  [flagged]
• swayvil 3y ago
  [flagged]
  • caymanjim 3y ago
    What a bizarre stance. It's literally easier to https-everything than it is to split your content up between http and https. And there are zero reasons to not use https. You come off as someone who couldn't figure out how to run certbot.
  • mrkeen 3y ago
    What symptoms did you run into?
    • deleted 3y ago
      [deleted]
• mprime1 3y ago
  Great read. Great product. I've been an early user of Antithesis. My background is dependability and formal distributed systems. This thing is magic (or rather, it's indistinguishable from magic ;-)). If they told me I could test any distributed system without a single line of code change, do things like step-by-step debugging, even rollback time at will, I would not believe it. But Antithesis works as advertised. It's a game-changer for distributed systems that truly care about dependability.
• chrsw 3y ago
  Could this work for embedded C projects? Bare metal or RTOS?
• deleted 3y ago
  [deleted]
• karatekidd32v 3y ago
  Not directly related to this post, but clicking around the webpage I chuckled seeing Palantir's case study/testimonial: https://antithesis.com/solutions/who_we_help https://antithesis.com/solutions/who_we_help
• norir 3y ago
  I think there is a lot of opportunity for integrating simulation into software development. I'm surprised it isn't more common though I suppose the upfront investment would scare many away.
• kendallgclark 3y ago
  Happy customer here —— maybe the first or second? Distributed systems are hard; #iykyk. Antithesis makes them less hard (not in line an NP hard sense but still!).
• binarymax 3y ago
  I got really excited about this, and I spent a little time looking through the documentation, but I can't figure out how this is different than randomizing unit tests? It seems if I have a unit test suite already, then that's 99% of the work? Am I misunderstanding? I am drawing my conclusions from reading the Getting Started series of the docs, especially the Workloads section: https://antithesis.com/docs/getting_started/workload.html https://antithesis.com/docs/getting_started/workload.html
  • jakewins 3y ago
    This is that, and the exact same vibe, except: it promises to keep being that simple even after you add threads, and locks, and network calls, and disk accesses and.. With this, if you write a test for a function that makes a network call and writes the result to disk, your test will fail if your code does not handle the network call failing or stalling indefinitely, or the disk running out of space, or the power going out just before you close the file, or.. So it’s; yes, but it expands the space where testing is as easy as unit testing to cover much more interesting levels of complexity
  • nlavezzo 3y ago
    Antithesis here - curious what part of the Getting Started doc gave you that impression? If you take a look at our How Antithesis Works page, it might help answer you question as to how Antithesis is different from just bundling your unit tests. https://antithesis.com/docs/introduction/how_antithesis_works.html https://antithesis.com/docs/introduction/how_antithesis_work... In short though, unit tests can help to inform a workload, but we don't require them. We autonomously explore software system execution paths by introducing different inputs, faults, etc., which discovers behaviors that may have been unforeseen by anyone writing unit tests.
    • binarymax 3y ago
      Thanks for the response. The linked introduction does help. The workload page does give me that impression (and based on upvotes of my post it does to others as well)...so perhaps disambiguating that the void test*() examples on the workloads page are not unit tests might help! Congrats on the launch and I'll consider using it for some of my projects.
• iamnotsure 3y ago
  "I love me a powerful type system, but it’s not the same as actually running your software in thousands and thousands of crazy situations you’d never dreamed of." Would not trust. Formal software verification is badly needed. Running thousands of tests means almost nothing in software world. Don't fool beginners with your test hero stories.
  • mrkeen 3y ago
    Great, but formal software verification is not yet broadly applicable to most day-to-day app development. Good type systems (a pretty decent chunk of formal software dev) are absolutely necessary and available. But things get tricky moving past that. I've tried out TLA+/PlusCal, and one or more things usually happen: 1) The state space blows up and there's simply too much to simulate, so you can't run your proof. 2) With regard to race-detection, you yourself have to choose which sections of code are atomic, and which can be interleaved. Huge effort, source of errors, and fills the TLA file with noise. 3) Anything you want to run/simulate needs an implementation in TLA+. By necessity it's a cut-down version, or 'model'. But even when I'm happy to pretend all-of-Kafka is just a single linkedlist, there's still so much (bug-inviting) coding to model your critical logic in terms of your linked list. Ironically, TLA+ is not itself typed (deliberately!). In a toy traffic light example, I once proved that cars and pedestrians wouldn't be given "greenLight" at the same time. Instead, the cars had "greenLight" and the pedestrians had "green"!
    • iamnotsure 3y ago
      "Colorless green ideas sleep furiously"
  • sfink 3y ago
    That'll work great for your Distributed QSort Incorporated startup, where the only product is a sorting algorithm. Formal software verification is very useful. But what can be usefully formalized is rather limited, and what can be formalized correctly in practice is even more limited. That means you need to restrict your scope to something sane and useful. As a result, in the real world running thousands of tests is practically useful. (Well, it depends on what those tests are; it's easy to write 1000s of tests that either test the same thing, or only test the things that will pass and not the things that would fail.) They are especially useful if running in a mode where the unexpected happens often, as it sounds like this system can do. (It's reminiscent of rr's chaos mode -- https://rr-project.org/ https://rr-project.org/ linking to https://robert.ocallahan.org/2016/02/introducing-rr-chaos-mode.html https://robert.ocallahan.org/2016/02/introducing-rr-chaos-mo... )
• mamidon 3y ago
  I can see how determinism can be achieved (not easy, but possible), and I can see how describing a few important system invariants can match 100's or 1000's of hand rolled tests, but I'm having a hard time understanding how it's possible to intelligently explore the inputs to generate. e.g. if I wrote a compiler, how would Antithesis generate mostly valid source code for it? Simply fuzzing utf8 inputs wouldn't get very far.
  • pfdietz 3y ago
    I don't know how they'd do compiler testing, but I know how I do it (testing Common Lisp), and can talk about that if you're interested. But it would be cool to hear how they'd do it.
  • chinchilla2020 3y ago
    The blog post has some impressive copy but is lacking details on how you implement their product. I am highly skeptical of any claims that something 'magically just works' without much configuration or setup.
    • intuitionist 3y ago
      (Disclosure: I’m an Antithesis employee.) The blog post is meant as a high-level introduction for a general audience. The documentation (https://antithesis.com/docs/ https://antithesis.com/docs/) goes into considerably more detail about what kind of configuration and setup you need to start testing with Antithesis.
• Gehinnn 3y ago
  Reading this article, I want the same now for js code that involves web-workers... How can I write code that involves a webworker in a way that I can simulate every possible CPU scheduling between the main thread in the webworker (given they communicate via post message and no shared array buffer)? Is it possible to write such brute force test in pure JS, without having to simulate the entire computer?
  • mrkeen 3y ago
    Use TLA+/PlusCal for this. It's what it's there for.
• gadders 3y ago
  This sounds amazing, but I wonder how long it would take to set up for any reasonably complex system.
• zoogeny 3y ago
  What is described in this post is the gold standard of software reliability testing. A world where all critical and foundational systems are tested to this level would be a massive step forward for technology in general. I'm skeptical of their claims but inspired by the vision. Even taking into account my skepticism, I would prefer to deploy systems tested to this standard over alternatives.
• mlsu 3y ago
  Pricing doesn't make sense. What does a CPU hour mean for this framework? How many do I need?
• ijustlovemath 3y ago
  We've done something similar for our medical device; totally deterministic simulations that cover all sorts of real world scenarios and help us improve our product. When you have determinism, you can make changes and just rerun the whole thing to make sure you actually addressed the problems you found. Another nice side effect is that if you hang on to the specification for the simulation, you only have to hang on to core metrics from the simulation, since the entire program state can be reproduced in a debugger by just using the same specification on the same code version.
• schaum 3y ago
  that sounds like "automated advanced chaos monkey" to me https://en.wikipedia.org/wiki/Chaos_engineering#Chaos_Monkey https://en.wikipedia.org/wiki/Chaos_engineering#Chaos_Monkey
  • nlavezzo 3y ago
    Depends on how far you mean with "advanced" here. We specifically cover the differences between Antithesis and Chaos Engineering in our "How It's Different" page: https://antithesis.com/product/how_is_antithesis_different/ https://antithesis.com/product/how_is_antithesis_different/ Here's the relevant text though: Antithesis testing resembles chaos testing, in that it injects faults to trigger and identify problems. But Antithesis runs these tests in a fully deterministic simulated environment, rather than in production. This means Antithesis testing never risks real-world downtime. This in turn allows for much more aggressive fault injection, which finds more bugs, and finds them faster. Antithesis can also test new builds before they roll out to production, meaning you find the bugs before your customer does. Finally, Antithesis can perfectly reproduce any problem it finds, enabling quick debugging. While chaos testing can discover problems in production, it is then unable to replicate them, because the real world is not deterministic.
• bell-cot 3y ago
  First reaction: "Yes, your site's weird font is bugging me!"
  • intuitionist 3y ago
    (Antithesis employee here.) We’re using Inter, which our designer assures me is pretty popular. But this isn’t the first time we’ve heard this complaint. Also, we had an issue in testing on a different part of our site where the font was getting computed as something weird and ugly on our development NixOS machines. Would you mind replying with what the browser console says your font is getting computed as? Thanks! Edit: The other person who mentioned this seems to think that it’s caused by their JavaScript blocker—we’re trying to figure out why, but in the meantime, enabling JS might help if you haven’t.
    • bell-cot 3y ago
      (It's JS blocking - I told NoScript to allow antithesis.com, and that completely changed the font in FireFox.)
• zubairq 3y ago
  I need to follow this example to build software faster
• ajb 3y ago
  I'm sure I've heard of something similar being built, but specific to the JVM (ie, a specialised JVM that tests your code by choosing the most hostile thread switching points). Unfortunately that was mentioned to me at least 10 years ago, and I can't find it.
• lifeinthevoid 3y ago
  I don’t want to sound silly, but there are 24 open and 37 closed bugs on the FoundationDB Github page. Could it perhaps be that bug-free is somewhat exaggerated? Antithesis looks very promising by the way :-) Edit: perhaps Apple didn’t continue the rigorous testing while evolving the FoundationDB codebase.
• jsdwarf 3y ago
  > and found all of the bugs in the database This is when I stopped reading
• hintymad 3y ago
  I really like antithesis' approach: it's non-intrusive as all the changes are on a VM so one can run deterministic simulation without changing their code. It's also technically challenging, as making a VM suitable for deterministic simulation is not an easy feat. On a side, I was wondering how this approach compares to Meta's Hermit(https://github.com/facebookexperimental/hermit https://github.com/facebookexperimental/hermit), which is a deterministic Linux instead of a VM.
• stavros 3y ago
  This is really impressive, but still, if you're working on a piece of software where this can work, count yourself lucky. Most software I've worked on (boring line-of-business stuff) would need as many lines of code to test a behavior as to implement the behavior. It's not very frequently that you have a behavior that's very hard to make correct, but very easy to check for correctness.
• shuntress 3y ago
  > a platform that takes your software and hunts for bugs in it Ok but, what actually IS it? It seems like it is a cloud service that will run integration tests. I have to figure out how to deploy to this special environment and I still have to write those integration tests using special libraries. But even after all that integration refactoring, how is this supposed to help me find actual bugs that I wouldn't already have found in my own environment with my own integration tests?
  • mrinterweb 3y ago
    I came away with the same questions.
  • spartanatreyu 3y ago
    The article says they created a deterministic hypervisor that runs all pseudorandom behavior from a starting seed to enable perfect re-playability. But that's all we know so far. I'm assuming there'll be some sort of fuzz testing, and static analysis or some defining actions that your software can perform. Honestly it sounds a lot like it has a lot of crossover with what the Vale language is trying to solve: https://vale.dev/ https://vale.dev/, but focused on trying to get existing software to that state instead of creating a new language to make new software already be at that state by default.
  • nlavezzo 3y ago
    I'd suggest taking a dive into the docs - there is quite a lot there that should address some of these questions. That said, Antithesis doesn't require you to write manual tests, integration or otherwise. It requires your software system to be packaged in containers, which is fairly straightforward, and then requires a workload to be written which will emulate the normal functioning of the software system. So for example an e-commerce store would have product views, cart adds, checkouts, etc. With this, Antithesis can start testing (running your workload, varying inputs, injecting faults, etc) the software and looking for violations of test properties. There are many (60+) test properties that come "out of the box" such as crashes, out of memory, etc. You can (and should) also define custom properties that are unique to your system, as this will surface more problems. As your tests run, violations of test properties are reported, with lots of useful debug information included. Test runs that are particularly interesting can have a lot of extra analysis done, due to our ability to "rewind" and change inputs, get artifacts, add logging, etc.
• mcapodici 3y ago
  So this is a valgrind for containers? "If" it works well, and doesn't flag false things, this is pretty useful. You might want to sell this as a bug finder. But it also could be sold as a security hardening tool.
• georgelyon 3y ago
  Congratulations to the Antithesis team! I actually interviewed with them when they were just starting, and outside of being very technically proficient, they are also a great group of folks. They flew my wife and I out to DC on what happened to be the coldest day of the year that year (we are from California) so we didn’t end up following through but I’d like to think there is an alternative me out there in the multiverse hacking away on this stuff. I highly recommend Will’s talks (which I believe he links in the blog post): https://m.youtube.com/watch?v=4fFDFbi3toc https://m.youtube.com/watch?v=4fFDFbi3toc https://m.youtube.com/watch?v=fFSPwJFXVlw https://m.youtube.com/watch?v=fFSPwJFXVlw
• JonChesterfield 3y ago
  > We thought about this and decided to just go all out and write a hypervisor which emulates a deterministic computer. Huh. Yes, that would work. It's in the category of obvious in hindsight. That is a very convincing sales pitch.
  • Smaug123 3y ago
    Along similar lines, Mario Carneiro wrote a formalisation of a subset of x86 in MetaMath Zero (https://github.com/digama0/mm0/blob/master/examples/x86.mm0 https://github.com/digama0/mm0/blob/master/examples/x86.mm0) with the ultimate goal of proving that the MetaMath Zero verifier itself is sound. https://arxiv.org/pdf/1910.10703.pdf https://arxiv.org/pdf/1910.10703.pdf (And of course Permutation City is a fiction book all about emulating computers with sound properties!)
• thisrod 3y ago
  I'm trying to figure out the name. Is it simply a play on Hypothesis, or am I missing something clever about this being the opposite of property-based testing?
• harshaw 3y ago
  I am really intrigued by organizations that build effective test cultures. I am not interested in people who have testing teams (ala how it was done before, say 2004) or teams that simply do unit tests and integration tests. I am interested in people who realized that building the right testing culture is key to their success. Before reading this article sqlite would probably be my top reference. I don't have the article handy, but the sqlite developers spend like a year building a test framework to make incredibly bulletproof software. I wasn't aware of foundationDB before but the idea of the simulation engine - that's exactly what most distributed systems folks need. disclaimer - I work at AWS. And we have a combination of TLA+, fuzz, and simulation testing. When I first started it was obvious my team had a huge testing gap. It pains me to say this but for a big part of AWS testing is sort of an after thought. It comes from the "we don't hire test engineers" mentality I suppose - but this likely differs wildly by team. Over the years we've tried to backfill the gap with simulators. But it is really hard to do this culturally. because it is really hard while you are trying to build new stuff, fix bugs, etc. And your entire team (and leaders) have to be bought into the foundational value of this infrastructure. And because we don't have it, we write COEs, we fix the obvious bugs, but do we take the 1 year it would take to avoid all problems in the future - no. So yeah I am super jealous of your "fully-deterministic event-based network simulation".
• martin82 3y ago
  This looks awesome, but what if my stack has a lot of buy-in into the AWS infrastructure and uses lambda, SNS, SQS etc... how to containerise this?? EDIT: Oh nice: https://antithesis.com/docs/using_antithesis/environment.html#aws-mocks https://antithesis.com/docs/using_antithesis/environment.htm...
• m3kw9 3y ago
  It sounds great but let’s see how it works and what are the constraints and what the UX looks loke
  • vojev 3y ago
    The UI is exposed on the website, you just have to poke around a bit. There's a link to a live report from this documentation page: https://antithesis.com/docs/reports/triage.html https://antithesis.com/docs/reports/triage.html
• rapjr9 3y ago
  I love this idea. In the early days of computing computers were claimed to always be deterministic. Give it the same inputs and you get the same outputs. Little by little that disappeared, with interrupts, with multithreading, with human derived inputs, with multitasking, with distributed processing, until today computers and applications are often not deterministic at all, and it does indeed make them very difficult to test. Bringing back the determinism may not only be good for testing, it seems likely to improve reliability. While I see how this is great for distributed databases I wonder if it has application when inputs are inherently non-deterministic (e.g., human input, sensor derived inputs).
• pulkitsh1234 3y ago
  alternative name for the product: Laplace's Demon for Your Code
• jongjong 3y ago
  Reminds me of my work in the blockchain space. I built a Decentralized Exchange which gets all of its inputs from blockchain data. Since all the inputs are deterministic (and it's all based in block time instead of real time), I can replay any scenario any number of times... But it goes one step further than what is mentioned in the article because I can replay any bug which ever happens, exactly as it happened, IN PRODUCTION. The output is also deterministic so all operations are idempotent; they can be replayed any number of times, going as far back in the past as you want and end up with exactly the same state. But, ironically, the DEX hasn't had any bug since it started operating 3 years ago... It makes debugging so easy, I was able to resolve every possible issue I could imagine before the launch. I think I haven't updated the code in a year but I've been running it this whole time and it's been processing trades. Another unusual feature is that you could technically trade between 2 blockchains while the DEX is offline... Even if the DEX is only restarted 1 year or decades later, it will resolve the trades as though the DEX had been online the entire time. Only difference is that the disbursement of funds will be in the future after the DEX is restarted.
• lysecret 3y ago
  Hmmm, so this excited me a great deal since I spent some time building a property-based testing system for a trading execution engine. (Which really can't have any issues). It's an agent-based system with many possible race conditions. Now, having built such a system (and being incredibly happy with it). I do not understand where antithesis comes in. Broadly there were 2 components: 1. A random strategy that gives random commands that are distributed in a very specific way. 2. Properties to test, observing the system (by listening to the messages) and checking them for some properties (like positions always being correctly protected etc..) Now, there is not much else (besides random trading data which is very easy to do or you can use actual live data). And all of them depend to 99% on domain knowledge. Now, where is there space for a company/generic framework to come in? I'm genuinely curious.
• tomerbd 3y ago
  Tactical 10x engineers - leave lot of mess and tech debt. Eventually this becomes 0.1X engineer. 0.5X strategic engineer will make the whole surrounding 2X engineers.
• xchip 3y ago
  The kids dieing in Gaza while our governments close one eye.
• deterministic 3y ago
  This is how I have always developed hard-to-make-bug-free software. Write a simulator first that will deterministically give your software the worst possible environment to run in with failures happening all the time. I have delivered complicated software into production using this method with zero bugs ever reported. It works brilliantly.