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

User settings, Lamport clocks and lightweight formal methods

jakub-m.github.io

Post reply on HN
Print view View original

11–20 of 22 posts

Re: User settings, Lamport clocks and lightweight formal methods

#11

Post by CGamesPlay »

So what is needed here is some sort of data type that is replicated, and guaranteed to converge. A convergent, replicated data type… a CRDT! In this case it rather seems like you wanted a regular-old time stamp, not a lamport timestamp, which gives you a “last-write-wins register” CRDT.

But perhaps you wanted something that actually handles the conflicts, like for a list of subscribers to an event. In that case you would want to use a vector clock instead of a lamport timestamp, and then when neither clock dominates the other (aka when they are tied), you take both sets and merge them. This is an incomplete outline of the “add-wins set” CRDT.

I wish CRDTs were more mainstream :)

Re: User settings, Lamport clocks and lightweight formal methods

#12

Post by arriu »

I’d encourage interested readers to look at some of Leslie’s other papers. His work from decades past was very forward thinking and useful in today’s world.

His work has directly shaped how many distributed systems reach consensus. Including recent projects like Solana. Also check out VDF and proof of history.

Re: User settings, Lamport clocks and lightweight formal methods

#14

Post by dboreham »

CGamesPlay wrote: post #11

So what is needed here is some sort of data type that is replicated, and guaranteed to converge. A convergent, replicated data type… a CRDT! In this case it rather seems like you wanted a regular-old time stamp, not a lamport timestamp, which gives you a “last-write-wins register” CRDT. But perhaps you wanted something that actually handles the conflicts, like for a list of subscribers to an event. In that case you w…

The "back end wins on un-ordered messages" scheme is a kind of vector clock, I suspect.

Re: User settings, Lamport clocks and lightweight formal methods

#16

Post by bluejekyll »

CGamesPlay wrote: post #11

So what is needed here is some sort of data type that is replicated, and guaranteed to converge. A convergent, replicated data type… a CRDT! In this case it rather seems like you wanted a regular-old time stamp, not a lamport timestamp, which gives you a “last-write-wins register” CRDT. But perhaps you wanted something that actually handles the conflicts, like for a list of subscribers to an event. In that case you w…

While I agree that CRDTs could work here, what struck me is you comment about a “regular-old timestamp”. In distributed systems, this isn’t simple. In fact, Lamport Clocks are a specific solution to guaranteeing a consistent monotonically increasing clock such that one time is known to occur after the other. A single instance, or primary db, can provide this, but in distributed systems this is the primary problem. There is no “regular-old timestamp” in distributed systems.

Re: User settings, Lamport clocks and lightweight formal methods

#17

Post by dmitriid »

User23 wrote: post #3

Interesting. Incidentally, I would claim that TDD done properly is in fact a lightweight formal method. It helps to be conversant with some kind of formal semantics, but you can definitely play a bit fast and loose by treating your tests as a lightweight specification. In that case any formal properties I want the code to have that can't practically be expressed in the test is included in a comment on the test. Also,…

> I would claim that TDD done properly

"I get paid for code that works, not for tests, so my philosophy is to test as little as possible to reach a given level of confidence" — Kent Beck

https://stackoverflow.com/a/153565

Re: User settings, Lamport clocks and lightweight formal methods

#18

Post by iforgetlogins01 »

TheTaytay wrote: post #2

Thanks for the article! I love lamport clocks, and the lightweight methods are cool. I read through the article a couple of times, and was unsure about something: When the browser resets, it does not appear to copy down the current state and clock value from the server, right? I'm basing that on this from the article: The browser resets, all the state is dropped. browser: settings: none, clock: 0 backend: settings: f…

(OP here) Thanks for the thoughtful comment!

Yes, you are right. To rephrase, you say that a browser could first increment its clock to the value larger that the backends, and then synchronize and "win" with the backend, setting the backend value to some bogus "none".

I'd say that it's "fine" in a way that the browser and the backend agree to "something" and are in sync. The case we wanted to prevent was that the browser and the backed hold different values and cannot agree which value to converge to.

Re: User settings, Lamport clocks and lightweight formal methods

#19

Post by MattPalmer1086 »

bluejekyll wrote: post #16
CGamesPlay wrote: post #11

So what is needed here is some sort of data type that is replicated, and guaranteed to converge. A convergent, replicated data type… a CRDT! In this case it rather seems like you wanted a regular-old time stamp, not a lamport timestamp, which gives you a “last-write-wins register” CRDT. But perhaps you wanted something that actually handles the conflicts, like for a list of subscribers to an event. In that case you w…

While I agree that CRDTs could work here, what struck me is you comment about a “regular-old timestamp”. In distributed systems, this isn’t simple. In fact, Lamport Clocks are a specific solution to guaranteeing a consistent monotonically increasing clock such that one time is known to occur after the other. A single instance, or primary db, can provide this, but in distributed systems this is the primary problem. Th…

Right. You can't guarantee clocks in a distributed system are synchronised, unless you control all the nodes. Lamport clocks don't use time, they work on causal order. This came after that, not this happened at a particular time.

Re: User settings, Lamport clocks and lightweight formal methods

#20

Post by CGamesPlay »

bluejekyll wrote: post #16
CGamesPlay wrote: post #11

So what is needed here is some sort of data type that is replicated, and guaranteed to converge. A convergent, replicated data type… a CRDT! In this case it rather seems like you wanted a regular-old time stamp, not a lamport timestamp, which gives you a “last-write-wins register” CRDT. But perhaps you wanted something that actually handles the conflicts, like for a list of subscribers to an event. In that case you w…

While I agree that CRDTs could work here, what struck me is you comment about a “regular-old timestamp”. In distributed systems, this isn’t simple. In fact, Lamport Clocks are a specific solution to guaranteeing a consistent monotonically increasing clock such that one time is known to occur after the other. A single instance, or primary db, can provide this, but in distributed systems this is the primary problem. Th…

Definitely true. In this case, where nodes are browsers (so clocks can easily be synced to within a few seconds of one another) and changes are user settings (so they change less than once an hour), a last-write-wins register seems like a great choice for an atomic setting like a boolean.

For settings where we can more intelligently handle conflicts (e.g. sets), we don't need the timestamps, because we can take advantage of vector clocks instead.

Post reply on HN