martinkl

Replaying immutable events in a deterministic order doesn't fit so well with Automerge; Automerge is more designed for apps where you can represent the mutable state of your application as an Automerge doc. https://livestore.dev/ might be a better fit for you.

Oh hi Andrew! It's been ages, hope you're well!

Hi there, good to hear from you! :)

Thank you! To your point about industrial use, yes – this is interesting. For example, Actyx makes a software system for coordination within a factory floor, and Ditto performs sync between devices of cabin crew on an aircraft. These are nice examples of industrial local-first systems.

Hi there! Martin here.

I agree that for most engineers, getting into formal proof is intimidatingly hard and perhaps not a good use of time, because lighter-weight specification languages and model-checking can help develop a good understanding of a system's behaviour with a much lower time investment.

But the intended audience for this post was not engineers working on production systems; it was intended for researchers studying distributed algorithms (e.g. consensus algorithms), and researchers who already know proof assistants and want to know how to use their skills to verify distributed algorithms. Note that this post appeared on a blog called "Machine Logic", not "Practical Distributed Systems Engineering"!

I have personally got a lot of value out of formal verification because the distributed algorithms I work on (CRDTs) are sometimes so subtle that without a proof of correctness, I simply don't believe that they are correct. I have several times developed algorithms that I believed to be correct, only later to find out that I was wrong. Here's a case study of one such example: https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-969.pdf

For people like myself, who are designing such algorithms, I believe that formal proof is worth the effort. But most people are not in this situation.

Hi, one of the authors here. You're right that in order to ensure that you won't receive timestamps lower than some threshold, you need to know all the nodes in the system, and you need to hear from all of them (if even just one node is unreachable, that will be enough to hold up the process). That's quite a big assumption to make, but unfortunately there doesn't really seem to be a good way around it. Lots of CRDT algorithms have this problem of requiring causal stability for garbage collection.

Using a consensus protocol is possible, and would have the advantage that it only requires communication with a quorum (typically a majority of nodes), rather than all nodes. However, it has the downside that now a node cannot generate timestamps independently any more — generating a timestamp would then also require a round trip to a quorum, making the algorithm a lot more expensive.

Not quite a MOOC, but if you like video, I published my lecture series here (same as what I teach to Cambridge undergraduates): https://www.youtube.com/playlist?list=PLeKd45zvjcDFUEv_ohr_H...

Martin here. I cited your paper in the related work section. It's a good start, but it does not cover everything that's required to achieve BFT — in particular, the issue that an operation may be valid in some contexts and invalid in others, and all correct nodes need to agree on whether an operation is valid or not.

If you have more details on the caveats you have discovered, it would be great if you could write them up so that others can learn from your experience!

Hello, Martin here :) I use the Paper app (https://wetransfer.com/paper) on an iPad, then transfer the images to a computer, do a little post-processing in Gimp and ImageMagick, and then drop the images into PowerPoint. You might be able to present directly from the Paper app, but it's more designed for drawing than for presenting.

For the first half on concurrent systems, videos are not publicly available (because the course is given by a different lecturer), but slides are available here: https://www.cl.cam.ac.uk/teaching/2021/ConcDisSys/materials....

Interesting idea, but the devil is in the details. Especially two concurrent moves of partially overlapping ranges of characters is a tricky case to handle, and it is not obvious to me how your scheme would deal with this.

Another fun case is two concurrent range moves in which the destination of the first move falls within the second move's source range, and the destination of the second move falls within the first move's source range. How do you handle this?

I expect that any algorithm solving this problem will need a formal proof of correctness, because it's very easy to miss edge cases when using informal reasoning.

Just for the record, I was already aware of GUN previously, and think it is a good project to include in the list. We had just forgotten about it when putting together this list of links. I guess I don't check HN all that often. ;)

I just looked up my own O'Reilly book on ebooks.com. http://www.ebooks.com/95729334/designing-data-intensive-appl... I can't see anything about DRM on the page, but under "supported devices" it says "e-readers with Adobe Digital Editions installed". Isn't that DRM enforcement software? Could you clarify please?

Edit: this page explicitly says that readers need to be compatible with Adobe DRM https://support.ebooks.com/hc/en-gb/articles/214119286-Guide...

I only have the blog post to go by, and don't have first-hand information. It seems possible to me that a few packets could indeed be delayed by 90 seconds, perhaps stuck in a switch buffer somewhere, although this would be a small number of packets since those buffers are not very big.

However, yes, I was thinking about the network stack as a whole. Any kind of retries, e.g. TCP retransmission on timeout, effectively turns packet loss into packet delay (within certain bounds). Thus, even if you have a network interruption ("partition") and all packets are dropped, it could happen that after the interruption is fixed, a node receives packets that were sent before or during the interruption. For this reason, I find it helpful to think of it as delay, not just packet loss.

The FLP result (Fischer, Lynch, Paterson) shows that consensus cannot reliably be solved in an asynchronous system (if you do not make any timing assumptions) if one or more processes can fail. The impossibility result shows that any consensus algorithm in such a system will have executions in which it waits forever and never makes a decision, which breaks the liveness property of consensus.

However, if you do allow some timing assumptions — just enough to measure a timeout, nothing more — then consensus becomes possible. In this case, the timeout is known as an "unreliable failure detector". See Chandra and Toueg's paper for details.

In a good algorithm, the safety properties do not depend on timing, only the liveness properties do. Rather than "consensus being impossible" perhaps it would be clearer to say "consensus may never terminate" in an asynchronous system. But "consensus impossible" is the standard way of phrasing this issue in the distributed systems literature.

There are some pointers to better terminology at the end of the post — e.g. I like Terry's session guarantees (read-your-writes, monotonic reads, etc) — but they too only cover a small subset of the design space.

In the end, this stuff is still evolving, and we simply don't yet know the best way of describing things. I wouldn't want to propose some alternative classification scheme that would be no better than the one it replaces. But I do want to encourage people to be precise and thoughtful with the terminology they use.

My beef with CAP is not that it's so broad, but that it's so narrow. It actually only proves a fairly small class of systems as impossible, and it's kinda obvious. Literature going back to the 1970s suggests that the trade-off was well known back then -- just not under such a catchy name.

Impossibility results are great, but misinterpreting them and using them to argue stuff to which they simply don't apply is not so great.

Oh, sorry to hear that it won't work in a follower. I guess I should have tested that before boldly claiming it :p

Apache 2.0 is just my default license to use for stuff. Would there be any conflict with the PG license?

Correct. If you're going to try it, I recommend getting a stylus for your iPad, since handwriting with your fingertip doesn't work very well.

Here are a few production users: https://cwiki.apache.org/confluence/display/SAMZA/Powered+By

The Metamarkets team wrote a nice post on their use of Samza a few days ago: https://metamarkets.com/2015/simplicity-stability-and-transp...

The problem is that, on the whole, users simply don't care. They have more important things to worry about than email encryption (you know, stuff like spouse, kids, mortgage, partying, etc).

The only way I can see end-to-end crypto really being adopted is if it's turned on by default everywhere. The selling point can't be the security, because people don't care about security -- the selling point has to be something else. Anything that requires a manual adoption step is going to automatically limit itself to a very niche audience.

The article is essentially arguing that entrepreneurs should be contrarian: not set up shop in the same place as everyone else, not try to hire the same people as everyone else, not have the same office setup as everyone else, etc.

Of course, to win, it's not sufficient to be contrarian — you have to be both contrarian and right. Whether or not these choices are right for you is probably highly dependent on what you're doing. But the idea of being contrarian, and not always following the received wisdom, is sound.

A tricky thing about communication is that sometimes it's really hard to convey why you believe something. You have some intuition that you should do A not B, but you can't put a finger on why. In order to resolve conflicts, you need to find a way of reasoning about intuition.

So I agree that open and honest communication is super important. I just wanted to note that difficulties in communication may happen even with the best intentions.

I don't know about Tesla specifically, but in general the security of embedded firmware is pretty catastrophic [1]. OTA updates are definitely a two-edged sword: on the one hand, they allow vulnerabilities to be fixed (without taking the car to a service center); on the other, the update process can itself be an attack target (e.g. man in the middle serves firmware image with malware included).

[1] https://www.usenix.org/system/files/conference/usenixsecurit...

This talk was mostly about backend systems, but it hints at Functional Reactive Programming at the end. That's a field in which people are working out how to update the UI based on event streams. Some cool projects to look at in this area are Elm, React and Meteor, for example.

Once you've got a UI that can be dynamically updated based on event streams, you can hook the backend streams into the UI using a WebSocket or similar.

Your first ("very unnatural") example is what I had in mind. And since read committed is the default isolation level in most RDBMS, it is prone to the lost update anomaly. (In MySQL, repeatable read is the default, but its implementation of repeatable read doesn't prevent lost updates.) Note I did point out that I'm referring to the default configuration, not the strongest supported isolation level.

Although your second example is probably what a human would write, an ORM framework would very likely generate a transaction looking like your first example.

Another example would be inserting a transaction into a table, and summing the transactions in the account in order to calculate the account balance. Making that safe requires preventing phantom reads, which means requiring serializability.

You say serializable costs very little in most situations. I can't claim to know what most situations are like, but all I know is that I've seen many people who have tried serializable and found it too slow for them. User a-priori gives an example elsewhere on this thread: http://www.michaelmelanson.net/2014/03/20/transactions/

My point is that weak isolation is very subtle, easy to get wrong, and you don't know that you got it wrong until it's too late. We need better understanding and better tools so that concurrency is less easy to screw up.

Nice example of a bug caused by weak isolation. FWIW, Postgres has an interesting implementation of "serializable" which takes far fewer locks than MySQL, so may give you better performance while retaining the same isolation level.

I don't know what behavior it "should" have. IMHO there's scope for different databases to implement things differently — otherwise there would be no room for innovation. The important thing is just that we understand precisely which guarantees we're getting and which we're not, so that we can write applications which behave correctly under a given isolation level. And that's the whole point of Hermitage.

What you describe is the Lost Update (P4) anomaly. It's in the test suite: https://github.com/ept/hermitage/blob/master/mysql.md#lost-u...

MySQL in repeatable read mode actually doesn't prevent this anomaly (it doesn't deadlock). You need to be in serializable mode to get the deadlock.