CRDTs and the Quest for Distributed Consistency

my name is Martin Chapman you might know me from this book that I published about a year ago called designing data intensive applications this book is not about CRD T's instead it's a very broad overview of the architecture of large-scale data systems and problems of distributed systems what I'm going to talk about today is a different area so I am a researcher at the University of Cambridge except today actually I am formerly on strike you might have you might have gathered I mean this seriously does there's a dispute going on at the moment at many UK universities where the powers that be want to essentially cut back our pension schemes in a very radical and unjustified way which amounts to a massive pay cut and really is not justified so as part of this I am on strike I'm still going to give to talk to you because our we have no problems with koukin it's our university that we have a problem with but just to say that I am giving this talk as a private individual who happens to be interested in distributed systems rather than ok so let's talk about some technical stuff so what I'd like to talk about is collaborative applications and so a classic example of this would be Google Docs so there as you know you can have several people who can all collaborate in a document they can edit the document at the same time without having to email this back and forth which is very convenient now what we want in this kind of systems is that eventually like even though several people might be editing the document at the same time they should all end up with the same document on their screen at the end so this is what we call a convergence property everyone should end up as they communicate having the same state so if you were here this morning Heidi Howard gave a great talk on consensus which is also about getting several nodes in the distributed system to agree on something and so it looks like superficially the problem that we have here is kind of similar to consensus so as we'll explain later in this talk act this is a very different kind of problem even though it looks superficially similar the properties that it has are fundamentally different and comparing those two will be an interesting part of this talk okay so let's take a scenario that is probably familiar to you this is you a little blue stick figure who is hacking on some code on your laptop and you make some changes you edit some source files you save them to your local disk at some point you decide you're ready to share this code with your colleagues and so you commit it to your favorite version control system and then you maybe push it to a centralized repository maybe to github or something like that some mechanism by which you can send your commits to your co-workers and so at the same time while you've been editing the code maybe your colleague who is this pink stick figure has also been editing the code has also been changing it maybe also making commits and what you end up now with is that if this colleague wants to also push their changes to the server they will first have to fetch that the commit that you pushed and have to merge those together and so as you've probably experienced before this kind of merge it's straightforward if you were editing two different files because in that case get just knows well two different files I'm just going to merge them together those changes are independent if one of you changed the top of a file and the other one changed the bottom of the same file then that's probably still fine as well because the changes are fine up in the part a part in the file that git just says okay I'll merge those automatically but if you were editing actually the same lines then you've got a merge conflict that you need to resolve manually so if we look at this kind of system more abstractly you can say there are a couple of nodes these might be like your laptop and your phone or they might be servers in a data center we don't really care too much there's some kind of computing nodes each of which can store some data and when you want to edit that data you make a change to your local copy which might like in the case of the source code is the source code files living on your local hard disk you change that and then at some point those changes get communicated to anyone else who also has a copy of that data so to any other nodes and so while this is going on maybe a purple user can simultaneously in making some change to their copy of the data and they similarly will then forward on those changes to the other users and so whether these these changes here are like wire gets pushed by this kind of explicit operation or if you're using Google Docs these kind of changes are sent automatically continuously in the background so in the case of Google Docs this the local copy that you apply the changes to is living in memory in your web browser so in the tab that you've opened the Google Doc in when you type a letter and you change the document that's change gets immediately applied to your local copy of the document so it doesn't wait for a round-trip to the server before showing the letter that you just typed on your own screen because that would take too long so what Google Docs does in that case is it immediately applies the change locally and then asynchronously in the background which might take a few seconds or whatever it sends on the meta change to the server will then sir sends on the change to anyone else who's got a copy of that document open and so you kind of get the same kind of property that several people can make changes independently without knowing about each other's changes just like you get with gits get commits just on a shorter timescale but you still have exactly the same concurrency issue in particular this concurrency issue becomes more obvious if you have offline editing so in this case you can think of this as a network partition that is separating one of the nodes from the rest of the system and so the pink user might still be changing the local copy their local copy of the document but they can't send the changes to any of the other users because they are offline right now they don't have an internet connection or because there's some network disruption and so in this case the changes will stay local to their own machine and then only sometime later once the network is restored those changes will then be flushed but what we still want in that case is for those changes to be merged together so taking this type of type of Google Docs again as an example you can let's take the state of the thing that is that we're working on as a text document so this is like just a sequence of characters which currently hello and so you have two users who can currently update this document the pink user adds the word the word world before the exclamation mark and the blue user adds a smiley face after the exclamation mark and so now if this was gits this would probably be a merge conflict that you would have to resolve manually but if you tried this kind of thing in Google Docs it turns out that actually Google Docs never prompts you to to resolve a merge conflict it will always just merge the changes automatically based on what it thinks is a sensible way of merging this and in this case we can actually define quite a sensible way of merging it because we can say well the world clearly came before the exclamation mark the smiley face came after the exclamation mark so we could just preserve both of those insertions and so a final sensible final merged state is hello world exclamation mark smiley and this is in fact what what Google Docs will do but we're not limited to only text documents so let's look at a different data type you could use a set for example so a set is just some unordered collection of elements and you could have the read user maybe removes the item B from the set so it was previously a B removes B so only a is left and concurrently while that is happening the purple user decides to add a new element C to the set written here with that set Union operator so the set then is merged ABC so as those two changes get propagated from one node to the other again we can set just define what we consider to be a sensible merged outcome and in this case I'm going to say well a was not touched by either user so we're just going to leave a there B was removed by all of the users C was added by one of the users so we want in the final state to contain C but not B and so we just say a and C is a sensible merged outcome in this case one more example I consider a counter so maybe like the number of likes on a Facebook post or something like that would be a counter that you can increment and so here let's say we're starting in the initial state where the counter value is one and you have two users who are both increment that counter so they both chained the value from 1 to 2 now you could say that's well both us design the same state so we should just continue we should just consider 2 to be the merged final states but that would actually lose information because here we know from inspecting the chain the set of changes that happened that actually to increment operations happened so really what we want is for both increment operations to still take effect in the final result so what we want is that the final result is actually three because we started in one and then one user incremented it the other user incremented it the order in which you do those two increments doesn't matter but the final value should be three so what this is saying is that we need to consider not just the state the value at any one time because if we just compare two and two they look the same but actually we need to capture the sequence of changes that were made to the data and we apply those and that will allow us to reach a sensible merged outcome okay so this problem of people editing stuff simultaneously and having to merge it has been studied for a rather long time and they are at a high level to families of algorithms that were developed one is operational transformation which has been studied by academics since the late 80s and which is actually the foundation of Google Docs so Google Docs internally uses an operational transformation algorithm however due to some problems that I'll explain in a minute people got rather frustrated with operational transformation in the early 2000s and then started this separate direction of research called conflict-free replicated data types or CRE T's for short and this is SEO duties has been the focus of our research so let me just give you a bit of historical background because it's kind of interesting and also some motivation for why we wanted C Aditi's so as I mentioned a whole bunch of people across research community have proposed operational transformation algorithms so the first ones in in the late 80s and you know the paper reads quite nicely and they kind of make sense and looks plausible when you read it except you do win then realize reading some more papers they're actually a few years after this was published people discovered that this application was this algorithm was simply wrong so what I mean with wrong is what these algorithms are supposed to achieve is convergence that is everybody ends up with the same document on their screen at the end if no more edits are happening however this algorithm did not achieve convergence attacked there were certain edge cases where certain edits could happen concurrently where you would end up permanently diverged so these two different copies would be permanently out of sync with each other and never become consistent again so that is kind of a problem so of course people thought about this a bit harder and proposed another algorithm unfortunately a few years later that one also turned out to be wrong it's had a very similar bug and this story just kept continuing so over the course of about two decades all of these algorithms were proposed and then of only a few later few years later to discover that it's wrong so a real bloodbath of failed algorithms here we did end up with a couple of algorithms which are correct and in fact Google Docs is based on one of those that is not wrong but the particular property of those remaining ones is that they require a centralized server so they restrict the communication flows in the system so that if the think user here changes something and the purple user has changed it's something the changes they make have to be exchanged via this central server so it's not allowed for them to have some kind of back channel or some kind of other communication paths on the side because if they had that they would break the consumptions of the algorithm and that it would no longer achieve this convergence so this is a severe restriction here all of the communication has to go by a Google server even if it's just like syncing some data between your phone and your laptop and they are like 50 centimeters away from each other you still have to go by a data center in Virginia or whatever which is kind of ridiculous if you think about it so what I'm interested in is generalizing this model so that actually you can just have any communication topology in the system so for example if the blue user here has two devices or a phone and a laptop and they want to synchronize some data the pink use also has two devices well they should just be able to synchronize by our local network or whatever connectivity they happen to have even if they're actually not connected to the internet right now so this kind of communication pattern is simply won't work in the google docs case because you cannot safely have this communication directly between devices without going through the central server so I think it's it would be really great if applications can not depend on this central server be more decentralized so that you can actually just use whatever network is available and then at some point later if connectivity is re-established then of course the node should be able to synchronize again using the Internet so this is a more kind of decentralized pattern for building applications and when I talk about decentralization people inevitably ask is that something to do with block chains because because a lot of people in the blockchain community who are interested in building these these systems without trust in a central server also label their their work under the heading of decentralization so I'm personally not all that interested in block chains I'm happy for other people to work on it but let me just compare the two briefly because it is such a frequently asked question so as you probably know a block chain consists of some blocks of data each subsequent block contains a hash of the previous block a cryptographic hash and that means then if you have a signature on the last block you can follow through the hashes and you're guaranteed the integrity of this entire sequence of blocks and then there might be some ugly trees and stuff like that which allow you to cryptographically prove that a certain record appears in this chain and so that's like the foundation for Bitcoin transactions and such like moreover what you have in most of these blockchain protocols is some kind of consensus protocol which decides what the next block in the chain is going to be and typically those are Byzantine consensus protocols which just means that they can tolerate some of the nodes actually being actively malicious and still despite the presence of malicious nodes this thing will agree on the next block so this agreement property is quite strong that you get in block chains so in particular what the protocol is supposed to guarantee is if there are no Forks you have this linear sequence of blocks it's a totally ordered sequence and there's this decision process which ensures that no conflicting transactions get put into the same block so what this means is if you're wanting to prevent a user from spending the same coin twice you have to make a decision as to whether this transaction or that transaction that they made using the same coin is the valid one so what you need here is consensus which if there are several conflicting proposed transactions it picks one and that is what prevents double spending in these cryptocurrencies so that is the fundamental abstraction of consensus there are several proposed values potentially conflicting and what the consensus protocol does is to decide on one of them and to throw away the others and that is exactly what you want in the case of a blockchain and it's exactly what you don't want in the case of collaborating on the document because if you think about it if you make some changes to a document and your colleague makes some changes to the document what a consensus protocol would do is to choose to do the changes from one of you and throw the other one away which is actually what it would probably make you a bit unhappy so what we want here for collaboration protocols is to keep all of the changes that were made and to merge them in such a way that they converge towards the same state so that is what I mean with this thing look superficially like consensus and is really different because consensus is fundamentally around this idea of choosing one okay so back to these two families of algorithms for achieving convergence I'm going to talk briefly about some research that we did on the oddities so the oddities are also a family of data structures which several people on different nodes can update concurrently and which will automatically merge the changes together very much like those examples I showed earlier anders talked and been used in a few practical systems so for example the autumn text editor just recently released a collaboration feature that is built on CRD T's the react database used them internally for merging things and so on so given this poor history of problems with operational transformation algorithms what we wanted to do is to be really sure that we're not repeating the same problems with CRD T's so we want to prove formally mathematically that the CR D T's really do converge that they really do behave as they're supposed to because as we saw with the problems with the OT algorithms some of these algorithms can be quite subtle and just like thinking about it unform aliy you might not be able to fully convince yourself that it really under all circumstances does converge so what we did is we used Isabel which is a theorem proving software which you can use to write down formally the properties that we want that you want and so we use this software to write down several CR DT algorithms so our GA is a is a text editing C R DT up set is a set and the counter is like what I showed earlier and we can show that they satisfy a consistency property called strong eventual consistency which in particular implies convergence and so we can show that these data types satisfy this consistency property under certain assumptions but now how do we know that those assumptions are valid we now have a second layer of proof in which we have a model of a network it's a very unreliable network it's allowed to throw away any number of messages reorder messages and what we prove here is that those assumptions under which this strong eventual consistency holds are satisfied in all possible executions of this network model so no matter how badly the network tries to mess things up we can prove that these algorithms will always satisfy the guarantees they claim so unfortunately I don't have time to talk about this theoretical work in any more detail if you're interested there's a URL there at the bottom of the paper it's reasonably readable even if you don't have prior experience in formal verification of algorithms so do have a look at what I do want to spend a bit more time talking about is Auto merge which is an application an implementation of these ideas that we've been working on this is an open source library in JavaScript in principle you could implement it in any language but guess JavaScript is very portable across many platforms which is why we're using that at the moment and you can think of this as a data model layer or data structure library on top of which you can build collaborative applications so what it gives you is a abstraction that looks very much like JSON and you can modify this JSON document and use that to build applications on top of it so I'll show you some examples of prototype applications that we built using this the first one is called trellis it's a clone of Trello the the popular project management tool looks like this so just like Trello you have columns and you have cards in those columns and you can drag and drop the cards between columns this year's a superhero recruiting initiative that we've used as an example and you can assign columns to people and you can leave comments on cars and so on all the typical stuff you would expect the cool thing with this is that it's implemented without any servers at all so we are able to do this based on a peer-to-peer networking model using WebRTC which is normally what enables like video calls in your web browser but you can use it for transferring data as well in particular we can transfer them edits made to a C R DT over something like WebRTC and as a bit of use interface here on the right hand side for managing that network and moreover what it does it keeps track of all of the changes that happened so whenever you move a card around or you update a card or whatever it actually appears in this log of changes here and on the bottom right hand side so that's just one example app that we built on top of auto mode another example is an app we call pixel pusher which is quite a fun one it's a collaborative pixel art editor so like pixel art is kind of sort of retro gaming aesthetic where you try to make pictures consisting from just this grid of a fairly small number of pixels and people like make really cute animations and stuff like that with this so we took this off-the-shelf open-source implementation by xavier balan i think is his name and this was just a user app running in your web browser and we made it turned it into a collaborative app by building on top of auto merge so it looks like this pixel pushes our variant and what we wanted to experiment with this here is not just like the straightforward collaboration where one user makes a change it shows up on another user's device but also wanted to think about like for example with git you get pull requests which is a mechanism by which a user can suggest some changes and then the maintainer of a repository can accept or not accept or maybe accept with some changes or with Google Docs there's this future for suggesting changes and making comments and so we wanted to explore a bit like what would a similar kind of suggesting changes like user interface look like for a collaborative pixel art editor so then in the top right hand side there's this bit of user interface where you can actually see there several different versions of the document so the base document contains just the eyeballs but then there's one variant that is like a potato man and so another variant and you can switch back and forth between those variants any user can create our own copy and then another user if they like it can merge that into their local kind of like a pull request but just with a very lightweight user interface so these kind of things are enabled simply by keeping track of the history of all of the changes that are done and that is what autumn urge does internally so as I said Auto merge is this kind of data structure abstraction on top of which you can build applications what emerged does not itself have a networking layer so it's just a piece of JavaScript that runs in one process it doesn't prescribe a way how that communicates with copies of the document running on other devices so we've now also been experimenting with different network layers that you can plug underneath what emerge so as I mentioned earlier trellis is built on top of web RTC peer-to-peer communication using a library that we called MPL the pixel pusher pixel art editor is actually built on a different networking layout because we were just experimenting with different layers this one taken from the DAT project so they are about a peer to peer synchronization of datasets it's a really interesting project so we were able to build on top of that using their long abstraction which actually worked really nicely as well so that's library called hyper merge which makes the connection between hyper call and Auto merge but if you like you can just send updates via server via WebSockets or what have you like really so autumn urge doesn't prescribe any particular network protocol for using here so let's look a bit more at the kinds of data structures you can use to build these collaborative applications so as I said Auto merge gives you this kind of JSON like abstraction and you can use JSON to implement for example a to-do lists so a to-do list consists on some fairly simple structures so in particular JSON has two ways of combining things together one is a list which is just an like an ordered sequence of things and one and the other is maps and so maps are just like a dictionary that map's a key to some value and the value can be again a map or it could be a nested sequence so you can nest these lists and maps inside each other arbitrarily and when you have this structure now you can modify it in several ways so for example you can change a value that appears somewhere so overwrite one primitive with another so setting and an item that's done like clicking the checkbox that this item is done would just trigger this flag here probably another thing you might do is edit a string that appears in here or you might insert a new item into a list between some existing items or you might like insert a new key into a map or you might remove things from this of course so you can do any sorts of editing operations on this data structure and in auto merge it looks like this so this is a some example JavaScript code of how you do this in auto mode so auto mode uses an immutable state object that is the State here is the current state of your data and that is never modified in place instead if you want to change it you call this water merged or changed function you pass in the current state and you get back a new object which is a new state in which steps new item has been reflected so it's very much like immutable J yes if you've used that kind of things it's a very similar way of thinking except what we wanted to try here is to keep a sort of familiar imperative programming model and so what we have here is you pass in this one thing you do is you can provide a kind of like a commit message we call it which is just arbitrary string it's not interpreted but it is stored alongside the editing history and so if you want to see what changes happened it's kind of nice to provide that sort of human readable explanation of the change and then there's this callback here where we have this document object which is mutable just within the period of this callback and any changes that you make within here are intercepted in JavaScript using a proxy object so here for example this to do is not push pushes the JavaScript or method for appending a new item to an array so it's here using the dock - duze doc dot - duze as an array appending this new item to the end of it and so these are just kind of standard javascript methods you can use assignment or whatever you like as well and autumn urge captures any of those changes and internally stores it as a log of operations so you don't normally have to deal with this operation log I'm just explaining it to you so you have a bit of an idea of what's going on under the hood and so internally this this one command here of adding a new to-do item gets broken down into these lots of little micro operations so what we do is we we create a new empty map object then we set the title key of that map object we set the donkey of that map object then we insert a place it create a new placeholder position in a list which is where we want to insert that to-do item and then we link that object we created into the list so fortunately you don't have to ever write these kind of operations yourself that would get extremely tedious but this is just to an idea of what's going on internally and now water merge simply remembers all of these operations forever and so this does use some storage but our basically of thinking there is that well gets if you ever get repository and you don't do a shallow clone actually the repository contains all of the commits that ever happened in that repository and so if gifts can keep all history forever then so can we and if we need to do compaction things in the future we'll solve that in the future but for now we're just storing everything and it's working surprisingly well actually and keeping all of the operations where ever has some really nice properties like we can do time travel so which sounds amazing it's actually really simple because we have all of the changes that happened we can look at past states of the document and so you can just ask for the history and it'll just give you a list of states that the document went through since the began in beginning of time and it'll keep the commit message that you attach to to any changes there there's human readable like add the to-do item and give you a snapshot of what the document was at that point in time and so auto mode is able to do this efficiently by just selecting the subset of operations at any given moment and figuring out from those operations what the document looked like at that time okay so we were talking about collaboration so let's talk about some concurrent changes because that's where the conflict resolution comes in so let's say that our starting point is two users both have this to-do lists can containing a single item which is watering the plants and it is not yet done and so two users now concurrently update this to-do list like maybe like one of them is me and the other one is my wife and we're sharing this to-do list between our two phones so for example maybe I add buying the milk which is done false and my wife says our she's watered the plants now so she marks that item as done and so these are two independent changes that happen maybe while the devices are offline so now we want to merge them together and so firstly we immediately apply any change to your local copy of the data of course that's what we want because even if you don't have an internet connection you should still be able to update the data obviously but then at some later the network comes back and we're able to communicate these changes from one device to the other and so at that point then Auto merge will figure out that well changes to two different objects we can merge these two together cleanly so setting done to true for the watering the plants get supplied to the left copy and inserting the new item of buying milk with done falls on the right hand side they both get applied and so in this case the merger is quite straightforward and what auto merge guarantees you this is the fundamental property of CR DTS is convergence and that is more formally defined if any two devices any two nodes have seen the same set of updates or the same set of operations even if they might have seen those operations in a different order as soon as they've seen the same set of operations then the state of the document will also be the same this is a really nice property to have because it means we're not depending on like who saw which operation in which order we just have this simple property that once the data has been exchanged everyone's in the same state now there are some edge cases in which there are conflicts that are not neatly result abour and this is really the only one actually that we can't sensibly resolve automatically which is the same field or the same item in the list it's overwritten with two different values and so like that's fundamentally the the most basic type of conflict and in this case you know it's not really defined is it better to buy soymilk or better to buy almond milk you know that could be a subject of debate and auto merge is not opinionated on whether soy or almond milk milk is better so what auto mage merge does is firstly it picks one of them arbitrarily but deterministically as the default value and so if you just like look at the document without inspecting conflict it'll just pick one of the two that's about the best we can do but it keeps the other one in the side object here called underscore conflicts and it will tell you hey you know there was a conflict for the field title and this other nodes node ID one two three four set the value to buy almond milk so even though we've got here buying soy milk as default value there's also this other one and so then it's up to the user interface do you want to show like both conflicting values and let the user choose one you can implement that kind of manual conflict resolution if you need to but this is actually this assignment to the same field is the only case in which that manual conflict resolution has to happen so if it's text editing for example let's say we've got an document that says hey guys and we may want to make it more gender-neutral so maybe one user changes guys to everyone the other user concurrently changes guys to folks and so you could say like how do we handle this kind of conflict and what auto modes does for this is in fact the same as what Google Docs would do in the same situation which is it thinks well ok guys was deleted on both replicas so delete it twice is the same as deleted once so guys is gone everyone was inserted on the left-hand side folks was inserted on the right-hand side if two things were inserted we're just going to keep both of them and we're just going to put them in an arbitrary order but we're going to make sure that the order is the same on all of the replicas so ensure that everyone sees either hey everyone folks or hey folks everyone I hope those is a valid merged outcome but which of the two gets chosen is non-deterministic sorry it's it's random but deterministic it's been chosen based on the unique identifiers of the nodes so like this is fundamentally the properties you get you might think it's not ideal maybe you do want more manual conflict resolution the basis on which we are going here is that actually like Google Docs does this and millions of people use Google Docs so it seems to be fine in many cases maybe what we want is kind of like an advisory conflict like notion that says that maybe if some edits occurred within like 20 characters of each other or whatever defines some kind of threshold that we show you a little note to the user saying by the way there were some edits close together here you might want to check if the most outcome is like a valid English sentence or not we can't figure that out but I think that's about as much conflict resolution as you might need here so I'd like to show you just briefly before we wrap up here held the algorithm behind this works because I think it's kind of neat and so although you don't need to implement this kind of algorithm yourself it's kind of cool to see what happens here so let's take as example a document consisting of the letters H e l and o and we have two concurrent edits happening to this document so one user adds a second L to make it reread hello and the user the other user the purple goos on the right adds an exclamation mark at the end so the way the CR DT works is it gives each character in the document a unique identifier and it has a particular scheme for creating those identifiers and that is it consists of a number which is just like a counter and the a and B here is the name of the node that created this particular list element so node a on the Left creates new list elements with a and node B here creates a new LMS tellement for B so using their name no to name me and so because each node increments the counter for every operation is generated and two different nodes will have different names so that makes these identify as unique across all of the nodes and so now when when these nodes exchange data might be viola server or any kind of network doesn't really matter what they exchange is these operations which say insert a new list element new character L with ID for a so that's the new the new ID given to this new element after the existing list element with ID to a so this is important it doesn't say like insert at position 15 because position 15 might change if somebody inserts or deletes something before position 15 so instead we use these identifiers as a way of reliably pointing to a particular position in the sequence and the other user similarly creates this operation that says insert exclamation mark with ID for be after the existing element 3 a which is the O and these messages simply get forwarded on to the to users and they each apply exactly what what you would expect so the purple one here looks for the character with ID 3a and puts the exclamation mark with 4p after the 3a so it doesn't matter that the position has shifted along by 1 this unique identifier still clearly identifies the position to where to insert and we just need this doesn't rely on any ordering guarantees particularly so this can just go through any kind of network so you might realize that I haven't told you about one of their issues which is what happens if two people insert in the same place in the same document and so this one requires a little bit more explanation so imagine we have a document that reads ABC and on the left hand side the user adds XY between the a and the B so it reads a XY BC and independently of that on the purple side the letters P and Q get added similarly between a and B and so what we want to ensure is that still here in this case everybody ends up in the same state at the end ok and so for this I'm now going to start with sending that that insertion of P over from the right hand side to the left hand side this works as you would expect so insert p with ID 4 be after 1a 1a is still there's the letter A so it puts the pede directly after a but before the X and then similarly the Q comes across insert Q with ID 5b after 4 B so for P is there bits there letter P that we just inserted so it puts the Q after the P okay so that's one direction sorted we've got a PQ x y BC now we need to ensure that if the message is going the opposite direction we end up in the same state and if we just do this naively so just applying say insert for a after one a it's actually going to end up with this in the in the opposite order on the right hand side so here we need to be a little bit more clever so we need to ensure that the X ends up after the Q so even though the the operation for inserting X says insert after 1a what we need to do is actually shift along and put it not directly after 1a but after 5b which it's a Q and so for that we're going to use the following rule when a new insertion comes in so in this case the insertion of for a comes in after 1a first of all we set to our starting position which is 1a so we want to insert after 1a and now we're going to compare the ID of the new incoming operation to the ID of the next element in the list and in this case at the next element is the is 4b that's the P and so what we're going to do now is if the ID of the incoming operation is less than the ID of the next element in the list we're going to skip over that element and move on so move one further to the right and we'll repeat the same thing so now we look at the next next element in the list which is Q Q has an ID of 5b 5b is also greater than 4 a so we're going to skip over it as well so apply the same rule skip over any of the elements that have a greater ID than the one we're inserting and so then we've skipped over Q now the next next element to look at is the letter B which has an ID of 2a 2a is less than 4 a so now we stop the skipping and this is where we insert the letter X and so this rule it does actually work it takes a little bit of convincing and this is why we did all of that for more proof stuff because it's not entirely obvious immediately that this actually does the right thing but it turns out that it does actually always do the right thing and now finally for the insertion of y this one is easy again because here now we have just insert y with ID 5 a after ID for a for a is that X that we've really placed in the list so now we can just put it directly after the X just to show you that the skipping doesn't happen in any other circumstances so this 5a is not going to skip over 2a because 2a is less than 5 a on the other side here this insertion of p4 will not skip over the X here because 4 P is greater than 4 a so for P you will not skip over for a ok so this whole thing is just an example of how the CR DTS work if you want to play around with this stuff what emerges open source and liberally licensed and it would be really great if anyone wants to try and just prototype some applications on top of it I'll tell you this is research code it's not production ready we're not pretending that it's perfect in all circumstances but it does seem to be working reasonably well we were able to build some non-trivial applications on top of it so maybe you will be able to as well thanks to especially the hyper core from the doc project which we used for the networking in our last work if you're interested in the formal verification there's a link to the paper this is this work is based on our earlier work on a Jason CR DT which is this penultimate paper here on the list except the algorithm we use in auto mode is actually a bit different from what is in the paper so we need to write an updated version of that with the latest algorithm but we haven't got around to that yet I'm afraid but there is a like a mock down page on the auto mode repository telling you about the internals if you're interested in that and finally this book which as I said it's not about CRD T's but might also be interesting to anyone thank you very much [Applause]

Channel: InfoQ

Views: 31,423

Keywords: Software Architecture, Artificial Intelligence, Machine Learning, Data Engineering, Consistency, Distributed Systems, Data, CRDT, Algorithms, InfoQ, QCon, QCon London

Id: B5NULPSiOGw

Length: 43min 39sec (2619 seconds)

Published: Mon Oct 01 2018