Surprised to see Venki mama on Onion!
11.08.2025 02:39 β π 2 π 0 π¬ 0 π 0@gowthamkaki.bsky.social
Assistant Professor at CU Boulder. Programming Languages. Formal Methods. Distributed Systems. Security. https://gowthamk.github.io
Surprised to see Venki mama on Onion!
11.08.2025 02:39 β π 2 π 0 π¬ 0 π 0Submitted a POPL paper without a single theorem. Yes, I like living life on the edge.
13.07.2025 16:40 β π 1 π 0 π¬ 0 π 0"If the NSF budget were to be enacted as is, it βwould spell the end of any pretence that the US leads the world in science and technology, handing that position to Chinaβ, says Neal Lane, who directed the agency under Democratic former president Bill Clinton." By @dangaristo.bsky.social 
π§ͺ
respects causal and arbitration orders simultaneously. What should take the priority in this case? (the above example is credited to @guiltygyoza.bsky.social ).
29.05.2025 17:35 β π 0 π 0 π¬ 0 π 0example is a counter that admits additions and multiplications. Suppose I want `add` to win over `mult`. How would I use this intuition to linearize the following partial order?:
           -> mult1 -> add2
        /
add1
        \
           -> mult2 -> add3
I don't see a linearization that...
E.g.., in an "add-wins" set, `Add(e)` is always ordered after a concurrent `Remove(e)`. This is easy because an `Add(e)` only ever conflicts with `Remove(e)` and vice-versa. But what if there are several kinds of conflicts? Is the arbitration order transitive/symmetric/anti-symmetric? A simple...
29.05.2025 17:35 β π 0 π 0 π¬ 1 π 0+1 also for lack of (principled) read semantics. In your demonstration of how an op-based CRDT is a semi-lattice of partially-ordered logs, it is assumed that concurrent ops are commutative. This is not always the case; an "arbitration order" is defined to order concurrent conflicting ops...
29.05.2025 17:35 β π 0 π 0 π¬ 1 π 0then we also need a buffer to store `Remove(e)` effects until preceding `Add(e)` effects arrive. This makes the implementation disproportionately complex compared to the simple spec of "add-wins" crdt, e.g., see the attached pic (from an earlier paper).
29.05.2025 17:12 β π 0 π 0 π¬ 1 π 0is received, it is applied only if the tagged vector clock is no less than eβs local vector clock, i.e., only if the arriving Remove has seen (i.e., causally succeeds) at least those `add(e)` ops the current replica is aware of. Otherwise it is a no-op. If casual delivery is not guaranteed ...
29.05.2025 17:12 β π 0 π 0 π¬ 1 π 0+1. Implicit causal delivery assumption is frustrating. Oftentimes the causality tracking mechanism is type-specific. E.g., in "add-wins" set, there need to be a vector clock for every element `e` to keep track of the number of `add(e)` operations executed on each node. When a `Remove(e)` effect ...
29.05.2025 17:12 β π 0 π 0 π¬ 1 π 0Another lecture on CPS and I had to mention @guannanwei.bsky.socialβs continuation.passing.style, as is the convention.
22.04.2025 23:48 β π 2 π 0 π¬ 1 π 0A few days ago I gave a keynote at the PaPoC workshop on Byzantine Eventual Consistency and Local-first Access Control. It wasn't recorded, but slides are here
speakerdeck.com/ept/byzantin...
DistSys/DB/PL/SE Folks: PaPoC 2025 CfP is out! Submit  papers or talk proposals on cool stuff you are working on these days!
papoc-workshop.github.io/2025/cfp.html