mad44

https://muratbuffalo.blogspot.com/2026/08/composition-and-mo... The rely-guarantee reasoning we used in this post is where the two abstractions meet and become a joint constraint. The modularity abstraction is the boundary: we split the specs into private versus interface variables, hiding produced from the consumer and consumed from the producer. The modeling abstraction is the Env actions. E.g., EnvPut is not an API for the producer, it is a reduction of the producer: the minimal behavioral skeleton of the entire producer relevant to the consumer's property.

Secondly, I think the open partial specs, composable specs would help address the problems with monolithic specs that Dodd's cites. https://muratbuffalo.blogspot.com/2026/08/composition-and-mo...

https://www.mongodb.com/company/blog/channel/engineering-blo...

And a couple more pearls from Prof. Winston here as well. https://muratbuffalo.blogspot.com/search?q=winston

https://muratbuffalo.blogspot.com

Sonification for monitoring and debugging distributed systems

In Search of an Understandable Consensus Algorithm. Diego Ongaro, John Ousterhout, Usenix ATC, 2014.

Papers We Love is a great resource, https://paperswelove.org/, if you like to get involved in a community to dip your feet into reading papers first.

This! This is so important.

Here is what I wrote (oh, wow, 10 years ago) about the process I use for reading papers. I hope it helps people.

https://muratbuffalo.blogspot.com/2013/07/how-i-read-researc...

The main benefit of the blog for me was to crystallize my understanding. Having forced myself to post in public, I try to write a simple and accessible summary. This leads me to realize the gaps in my understanding, and fill them. This also strengthens my understanding, because by explaining the work in my own words, I internalize the concepts better. When I revisit a paper I have read before, the difference between a paper I wrote a post about and one I just read for myself is clear as day and night. I have a much better recall about the paper I posted. For a paper I wrote a summary, I just go to my summary and am able to cache back in all my understanding of the paper to my brain with a quick re-read of my summary.

This being said, I also benefited in terms of networking and collaboration. Through the blog post discussions on Twitter, I made many friends who work on distributed systems and databases. I think the blog was also useful for getting me a sabbatical at Microsoft Azure CosmosDB in 2018.

Finally, it feels really good to share my learnings, and put my rough ideas in the open. I learn from other blogs, and it feels good to give back. Every couple months I would get an email, thanking me for my blog, and that means the world to me.

I get it now. It is all thanks to separating the operation as 1. agreeing on WAL, 2. executing after waiting all WAL agreements stabilizing.

There is a separation between the two. This can introduce waits (which could be theoretically unbounded for EPaxos but Tempo and Accord bounds this).

Maybe in some sense this is in the same spirit of Calvin's serializing WAL first and executing it later. But Accord avoids a single entity doing the serialization and achieves it via a leaderless Paxos approach which uses dependency graphs for WAL serialization, and later using another protocol for WAL execution after settlement.

w2 may hit different nodes than w1 in a sharded database?

Or is the leader-Paxos approach in Accord operate over all nodes in the database regardless of the shards the keys fall into? (I guess that is the only explanation.) But then scalability of these global transactions would be limited, no?

Thank you for your detailed explanations.

;; one sentence per line

(defun wrap-at-sentences ()

  "Fills the current paragraph, but starts each sentence on a new line."

  (interactive)

  (save-excursion

    ;; Select the entire paragraph.

    (mark-paragraph)

    ;; Move to the start of the paragraph.

    (goto-char (region-beginning))

    ;; Record the location of the end of the paragraph.

    (setq end-of-paragraph (region-end))

    ;; Wrap lines with 'hard' newlines (i.e., real line breaks).

    (let ((use-hard-newlines 't))

      ;; Loop over each sentence in the paragraph.

      (while (< (point) end-of-paragraph)

        ;; Determine the region spanned by the sentence.

        (setq start-of-sentence (point))

        (forward-sentence)

        ;; Wrap the sentence with hard newlines.

        (fill-region start-of-sentence (point))

        ;; Delete the whitespace following the period, if any.

        (while (char-equal (char-syntax (preceding-char)) ?\s)

          (delete-char -1))

        ;; Insert a newline before the next sentence.

        (insert "\n")))))

;; one sentence per line (defun wrap-at-sentences () "Fills the current paragraph, but starts each sentence on a new line." (interactive) (save-excursion ;; Select the entire paragraph. (mark-paragraph) ;; Move to the start of the paragraph. (goto-char (region-beginning)) ;; Record the location of the end of the paragraph. (setq end-of-paragraph (region-end)) ;; Wrap lines with 'hard' newlines (i.e., real line breaks). (let ((use-hard-newlines 't)) ;; Loop over each sentence in the paragraph. (while (< (point) end-of-paragraph) ;; Determine the region spanned by the sentence. (setq start-of-sentence (point)) (forward-sentence) ;; Wrap the sentence with hard newlines. (fill-region start-of-sentence (point)) ;; Delete the whitespace following the period, if any. (while (char-equal (char-syntax (preceding-char)) ?\s) (delete-char -1)) ;; Insert a newline before the next sentence. (insert "\n")))))

(global-set-key (kbd "M-j") 'wrap-at-sentences)

https://muratbuffalo.blogspot.com/2018/03/change-my-mind-abo...

I don't see any better arguments, development put forth since then