318indexindex.xmlChris Jensen's Forest I am a distributed systems researcher, focusing specifically on simplifying the underlying protocols for strongly consistent distributed databases. 241cjj39-0005cjj39-0005.xmlConsensus2024714Chris Jensen167cjj39-0001cjj39-0001.xml$F+1$ systems are all you needArticle2024713Chris Jensen Currently consensus requires 2f+1 at least for consensus. Unless you require 100% uptime, this is unnecessary and consensus can instead function on F+1 replicas. 169cjj39-0002cjj39-0002.xmlFailure and recovery in $f+1$ and vertical paxosRemark2024714Chris Jensen Supposing the standard approach of VerticalPaxos and an external configuration manager. Here failure of any node blocks the cluster, since it is not failure masking. 171cjj39-0003cjj39-0003.xmlConfiguration manager is strictly weaker than SMR and consensusHypothesis2024714Chris Jensen Looking at FLP result and verticalpaxos consider the following system. Each config replica maintains an infinite array of configuration, and counter for virtual synchronous leases. A reconfiguration manager contacts a majority of replicas, proposing a virtually synchronous lease for it. Each config replica only provides the lease if it is the highest so far. Once receiving the lease, the RM reconfigures, then writes into the array at the index of the lease the new configuration. Reading the newest configuration is simply reading a majority of replicas and then using the highest configuration. The question is whether this is FLP avoiding, similar to read-write registers. 173cjj39-0004cjj39-0004.xmlWhat is the simplest to run configuration manager?Remark2024714Chris Jensen One important point in VerticalPaxos is that the configuration manager only need to be able to provide the current configuration, and to provide monotonically increasing configurations where each one knows of all lower ones. The simplest automated form of this is just a single oracle server. However in practise the actual simplest form of this is just a single human brain. Supposing that this user is the only user of the system, then we can use an F+1 configuration, with manual reconfiguration whenever a replica fails. 175cjj39-000Lcjj39-000L.xmlMonotonic systems are easierArticle202618 If your state is monotonic then caching becomes trivial. If your value is also monotonic then you can reason about second hand knowledge (known to be known). 243cjj39-0008cjj39-0008.xmlAdvice20241123Chris Jensen238cjj39-0007cjj39-0007.xmlSyntax highlighting and unicode for tla+ in papersAdvice20241123Chris Jensen TLA+ unicode is well done via https://github.com/tlaplus-community/tlauc Syntax highlighting is more difficult with unicode in latex. Since latex listings does not support unicode, and cannot be made to support unicode for syntax highlighting, you are left with minted. The issue is that minted does not support tla out of the box, and minted does not support custom pygmentise parsers easily. Solution: Use chromacolor, https://github.com/TomLebeda/chroma_code, with the relevant tree-sitter grammar already loaded. Note that the latest tree-sitter-tla does NOT support tree-sitter <0.25, so ensure you have at least this version (2024-11-23). 245cjj39-0009cjj39-0009.xmlRandom-theory20241123Chris Jensen228cjj39-0006cjj39-0006.xmlRummikub is solvable using a normalised formConjecture202482Chris Jensen The idea is that there are two normalised forms of any rummikub board which can be simply converted between. One which maximises the tiles in the runs, and one which maximises the number of tiles in duplicates. The conjecture is that if a tile is placable, it will be directly placable in one of these two normalised forms. 230cjj39-000Acjj39-000A.xmlAutomation and Augmentation. or: Alienation and Agency2024125Chris Jensen A recent blog post made the comment that current technology is alienating as it removes agency. Although this could be an effect of the current enshitification game-plan of tech companies it could also come from the aim of the tech itself. 202cjj39-000Bcjj39-000B.xmlAutomation2024125Chris Jensen The purpose of automation is to make an action or job take less time. For example, an automated assembly line's purpose is to remove the humans from the assembly line and hence reduce labour costs and by now has also resulted in improved speed of assembly lines. 204cjj39-000Ccjj39-000C.xmlAugmentation2024125Chris Jensen Augmentation aims to allow people to do a job better. For example, in the driving space, ABS, adaptive cruise control and lane keeping have been very very successful, and allows drivers to pay more attention to the drivers around them while still acting reasonably when there is an issue. Augmented systems have the following important characteristic. They tend to be continuous. Supply them input similar to previous inputs and they will produce similar outputs. In practise this means that humans can learn how these systems react and rely on that reaction. This gives users agency in preemptively correcting unwanted actions. My thesis is that since the primary aim of automated systems is to make an action or job take less time, its compatibility with human operators is not a primary design goal. Hence these systems do not provide affordances for humans, alienating them and removing their agency. Instead we can build systems to augment operators, allowing them to perform tasks better. We currently have many AI systems which aim to automate many things. However, the affordances arising from these systems are markedly discontinuous. Especially the current crop of AI systems which actively use randomness to 'mix up' the output. 206cjj39-000Dcjj39-000D.xmlJob loss through automation2024125Chris Jensen Historically job losses have occurred when things have been automated, however those have primarily been because the 'effectiveness' of another job has consumed an existing job. For example, excel empowered regular people to the point that accountants became largely unnecessary for regular finances. MS word empowered regular writers and people, to remove the job of the copy editor. 208cjj39-000Ecjj39-000E.xmlAI automation and augmentation of Doctors2024125Chris Jensen Automation: Looking at a picture of a tumor to decide if its cancerous. Augmentation: rescaling pictures to be consistent and giving them false color to visualise other datapoints 210cjj39-000Fcjj39-000F.xmlAI root cause analysis2024125Chris Jensen Automation: "What is the cause of this bug" Augmentation: "Static analysis to overestimate the codepaths which could trigger the bug" Augmentation: "Logs filtering to automatically remove 'normal' messages" Conclusion. My hope is that we can move from aiming to build automagic solutions to instead build augmenting solutions. To adapt a quote from RainWorld. With AI automation we have put our faith in the hands of Random Gods.