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

1–10 of 22 posts

Re: User settings, Lamport clocks and lightweight formal methods

#2

Post by TheTaytay »

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: foo, clock: 2
I don't think that lamport clocks can be compared if they are not representing any concept of causality or knowledge, right? This implementation appears to be two separate integers (one for the client and one for the server), with no guarantee as to their ability to communicate with each other. One bug you discovered was that the server might have a value 2, and the client might have a value 2, but they would disagree on the state that value "2" referred to. A bug indeed! Your fix was to handle the case where the client and server tied. However, I was left wondering: What about the case where the knowledge of the client is higher than the server, but the server still should not trust it? What if, in your example step 4, the client had made 3 changes without the ability to sync with the server? It would be this:

  The user changes the settings three times, but this time the state is not propagated to the backend (e.g. due to network hiccups).
  browser: settings: none, clock: 3
  backend: settings: foo, clock: 2
In that case, by the time the client talks to the server, the server would think that the client had "won", but the fact that the client had a clock value of "3" would be meaningless, right? Wouldn't you still want the server to win in this case?

Re: User settings, Lamport clocks and lightweight formal methods

#3

Post by User23 »

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, fuzzing is a way to narrow that gap further.

Re: User settings, Lamport clocks and lightweight formal methods

#4

Post by subleq »

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,…

A failing test can only prove the existence of a bug. A passing test can not prove that there are no bugs.

Re: User settings, Lamport clocks and lightweight formal methods

#6

Post by mjb »

danuker wrote: post #5

Can't help but think that this "logical clock" doesn't care simultaneity is relative. Ingenious!

Yes, that's exactly right. Lamport clocks provide a partial ordering of events, based on the idea of "happened before". Specifically, Lamport defines the happens before operator →, such that within any one thread/process if a is done then b is done then a→b, and if a is one process sending c message and d is another process receiving the message then c→d. This allows a model where single-threaded processes communicate through messages, and allow us to reason about things like "if a could have caused b to happen, then a→b". Logical clocks are an extension of this model.

This is covered in the classic "Time, Clocks" paper (https://www.microsoft.com/en-us/research/uploads/prod/2016/1...). If you read exactly one distributed systems paper in your life, it should probably be this one.

Re: User settings, Lamport clocks and lightweight formal methods

#7

Post by mjb »

mjb wrote: post #6
danuker wrote: post #5

Can't help but think that this "logical clock" doesn't care simultaneity is relative. Ingenious!

Yes, that's exactly right. Lamport clocks provide a partial ordering of events, based on the idea of "happened before". Specifically, Lamport defines the happens before operator →, such that within any one thread/process if a is done then b is done then a→b, and if a is one process sending c message and d is another process receiving the message then c→d. This allows a model where single-threaded processes communicat…

Bonus all-time great paper review: "Jim Gray once told me that he had heard two different opinions of this paper: that it’s trivial and that it’s brilliant. I can’t argue with the former, and I am disinclined to argue with the latter." (from Lamport at https://www.microsoft.com/en-us/research/publication/time-cl...).

Re: User settings, Lamport clocks and lightweight formal methods

#8

Post by pydry »

subleq wrote: post #4
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,…

A failing test can only prove the existence of a bug. A passing test can not prove that there are no bugs.

Neither can a formal spec.

Re: User settings, Lamport clocks and lightweight formal methods

#9

Post by User23 »

subleq wrote: post #4
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,…

A failing test can only prove the existence of a bug. A passing test can not prove that there are no bugs.

Believe me, I take Dijkstra's message to heart. And a quality test suite can reify the decisions of a formal specification as expressed in PTS or some other suitable abstraction. Think more here's the proof, more or less rigorous as circumstances suggest reasonable, and here's some tests that capture as much of that in code as practicable to help give us some further confidence that we didn't err in our manipulations.

Re: User settings, Lamport clocks and lightweight formal methods

#10

Post by User23 »

pydry wrote: post #8
subleq wrote: post #4

Earlier quoted context omitted.

A failing test can only prove the existence of a bug. A passing test can not prove that there are no bugs.

Neither can a formal spec.

That's a category error. The formal spec isn't a proof, it's what is to be proven. Without a spec the notion of programming errors has no formal meaning. In that case, the complaints about the bug are always with respect to pleasantness. Given a formal specification, it's possible to write a program that will reliably satisfy that specification. And the tooling is better than ever. The Dafny language out of Microsoft Research is one interesting example. One can also do it by hand, possibly using an SMT solver to check one's work.
Post reply on HN