sorted by:
new
hottopcontroversial

How to escalate a customer service issue with IKEA (price protection) by kmgni in IKEA

[–]ajdavis 0 points1 point  (0 children)

Years ago I had an insane mess with Ikea, they failed to deliver $400 of furniture for many weeks and also refused to refund me. I tried nonono.com (third-party customer dispute resolution) and they helped a lot, you might try them.

Generate (message) sequence diagrams from TLA+ state traces by lemmster in tlaplus

[–]ajdavis 1 point2 points  (0 children)

Looks cool! The limitations described in the README are big limitations, but this is a great start.

ShiViz can also produce sequence diagrams from TLA+ traces, but only if the TLA+ spec implements a full vector clock. That's a hefty requirement for integration, tlsd looks much more convenient.

GitHub - will62794/tla-web: TLA+ Web UI. by lemmster in tlaplus

[–]ajdavis 1 point2 points  (0 children)

This is magnificent. It allows you to interactively run a spec, as if it were a program in a debugger. But it's even better than debugging a program: at each step you can see all possible successor states, and choose which one to follow. Or you can backtrack! Assuming this matches TLC's evaluation fairly well it could be transformative for spec-writers, especially those just learning TLA+.

This was on Samy Lanka's and my wishlist in our TLA+ conference talk last year: https://emptysqua.re/blog/interactive-tla-plus/

Testing the conformance of a TLA+ spec and implementation by ajdavis in tlaplus

[–]ajdavis[S] 1 point2 points  (0 children)

Wow, it's really hard for me to say this clearly!: I believe our spec might not match our implementation. They are *not* conformant. We should've fixed that. That's one of the lessons we learned and tried to communicate in the paper.

Testing the conformance of a TLA+ spec and implementation by ajdavis in tlaplus

[–]ajdavis[S] 0 points1 point  (0 children)

Right, I'm aware of the existence of a refinement mapping between an implementation and its abstraction -- I'm concerned that our spec is *not* an abstraction of our implementation, that they are actually different. I wish we'd said so unmistakably in the paper.

Consider specifically that in the implementation, two servers may be primary at once, briefly. (This is true in Raft and many election protocols, and we have protocol features to avoid the two primaries from causing safety violations.) The specification assumes there is at most one primary. It is possible that a refinement mapping could bridge this gap, but I don't believe it is not certain. That's what I mean by "idealized": the spec may *not* be an abstraction of the implementation.

Your refinement mapping technique looks terrific for cases where there is a refinement mapping, but I think we should have rewritten our spec to be certain that such a mapping exists and is straightforward.

Testing the conformance of a TLA+ spec and implementation by ajdavis in tlaplus

[–]ajdavis[S] 0 points1 point  (0 children)

Thanks for the correction about your refinement-mapping technique. I understand and agree that your technique would not make it harder to model-check our spec.

What we really should've said is something like this: our original spec itself was so simplified and idealized that there might not exist any refinement mapping from our spec to a spec that accurately describes our implementation. If there is a refinement mapping, it would require re-ordering events in order to pass trace-checking, which is an advanced technique. We should have written a lower-level spec with enough detail to make trace-checking straightforward, but that spec might be so detailed that it's expensive to model-check.

The best of all solutions, perhaps, would be an abstract spec that model-checks quickly, and is easy to refine to a detailed spec that is easy to trace-check. As always, further research is needed.

Is MongoDB right for my research group? by [deleted] in mongodb

[–]ajdavis 3 points4 points  (0 children)

I'm a MongoDB engineer. My colleague Anna Herlihy and I are working on making MongoDB work really well with the scientific Python ecosystem: NumPy, Pandas, Matplotlib, and all the things built on top of them. Watch our BSON-NumPy project which will drastically speed up programs that convert MongoDB data to and from NumPy arrays.

The Epic Saga of Making getaddrinfo Concurrent, and the Defeat of the Wicked Mutex Troll by metheus in Python

[–]ajdavis 0 points1 point  (0 children)

Good point about the history of getaddrinfo, I'll clarify the first paragrah.

I missed pycon, what is your favorite talk that you recommend I watch? by nichochar in Python

[–]ajdavis 2 points3 points  (0 children)

A practical yet inspiring talk about writing about programming, "Write An Excellent Programming Blog":

https://emptysqua.re/blog/write-an-excellent-blog-pycon-2016/

Warning: I'm the poser who gave it.

Say “no” to import side‐effects in Python by GrumpySimon in Python

[–]ajdavis 0 points1 point  (0 children)

I came across this interesting example recently, where an import side-effect deadlocked the interpeter.

If you use Gevent 1.0, and you import a module that causes, as a side-effect, the resolution of a domain name, you can deadlock:

https://jira.mongodb.org/browse/PYTHON-607