Aneris: A Mechanised Logic for Modular Reasoning about Distributed Systems
This is a modal window.
Das Video konnte nicht geladen werden, da entweder ein Server- oder Netzwerkfehler auftrat oder das Format nicht unterstützt wird.
Formale Metadaten
| Titel |
| |
| Serientitel | ||
| Anzahl der Teile | 13 | |
| Autor | ||
| Lizenz | CC-Namensnennung 3.0 Deutschland: Sie dürfen das Werk bzw. den Inhalt zu jedem legalen Zweck nutzen, verändern und in unveränderter oder veränderter Form vervielfältigen, verbreiten und öffentlich zugänglich machen, sofern Sie den Namen des Autors/Rechteinhabers in der von ihm festgelegten Weise nennen. | |
| Identifikatoren | 10.5446/54927 (DOI) | |
| Herausgeber | ||
| Erscheinungsjahr | ||
| Sprache |
Inhaltliche Metadaten
| Fachgebiet | ||
| Genre | ||
| Abstract |
| |
| Schlagwörter |
5
12
00:00
DistributionenraumProgrammProgrammverifikationHardware-in-the-loopFormale SpracheRechnernetzDatenparallelitätSocket-SchnittstelleMathematische LogikGrenzschichtablösungModul <Datentyp>Partielle DifferentiationSystemprogrammierungPhysikalische TheorieFramework <Informatik>BeweistheorieNotepad-ComputerThreadInvarianteProtokoll <Datenverarbeitungssystem>Gerade ZahlKnotenmengeTelekommunikationArithmetischer AusdruckSocketIntegritätsbereichAdressraumMessage-PassingAdditionServerClientImplementierungMathematische LogikGrenzschichtablösungPhysikalisches SystemModul <Datentyp>AlgorithmusDigitaltechnikOrdnung <Mathematik>SoftwareTelekommunikationProgrammierungHalbleiterspeicherTypentheorieInvarianteKategorie <Mathematik>Funktionale ProgrammierspracheTropfenSynchronisierungProgrammierumgebungProgrammverifikationAggregatzustandAussage <Mathematik>BeweistheorieEinfach zusammenhängender RaumFunktionalGruppenoperationKomplex <Algebra>LeistungsbewertungMereologieMultiplikationResultanteSpeicherverwaltungStellenringStichprobenumfangVirtuelle MaschineWarteschlangeZahlenbereichServerExogene VariableParametersystemCoprozessorSerielle SchnittstelleCASE <Informatik>Prozess <Informatik>Zusammenhängender GraphAbstraktionsebeneZeiger <Informatik>Notepad-ComputerSummierbarkeitAdditionNetzadresseInformationsspeicherungProtokoll <Datenverarbeitungssystem>ThreadPrädikat <Logik>UmwandlungsenthalpieRahmenproblemArithmetischer AusdruckPartielle DifferentiationFramework <Informatik>AdressraumSchnelltasteClientInterleavingDifferenteKontrast <Statistik>NeuroinformatikDatenparallelitätKlassische PhysikSocketKontextbezogenes SystemMultiplikationsoperatorSchlussregelFreewareURLMessage-PassingMapping <Computergraphik>Dienst <Informatik>MusterspracheXMLUMLComputeranimation
08:00
ServerClientSocketAdditionProtokoll <Datenverarbeitungssystem>Message-PassingProgrammverifikationPhysikalisches SystemVertikaleImplementierungProgrammbibliothekPhasenumwandlungProgrammWeb-SeiteMathematische LogikOrdnung <Mathematik>GrenzschichtablösungModul <Datentyp>ABEL <Programmiersprache>ROM <Informatik>Physikalischer EffektDatenbankFormale SprachePhysikalische TheorieIRIS-TBeweistheorieNotepad-ComputerFramework <Informatik>SystemprogrammierungSkalierbarkeitPartielle DifferentiationBeobachtungsstudieCodeDatenbankDatensatzDigitaltechnikImplementierungMathematische LogikOrdnung <Mathematik>ProgrammierspracheProgrammierungProgrammbibliothekMAPKategorie <Mathematik>ProgrammverifikationGrenzschichtablösungBeweistheorieEinfach zusammenhängender RaumFunktionalGeradeInhalt <Mathematik>LoopMaßerweiterungMultiplikationPhysikalische TheoriePhysikalisches SystemProjektive EbeneResultanteStellenringZahlenbereichServerExogene VariableSerielle SchnittstelleCASE <Informatik>Prozess <Informatik>Zusammenhängender GraphAbstraktionsebenePräkonditionierungZeiger <Informatik>Notepad-ComputerSummierbarkeitAdditionNetzadresseLastteilungEin-AusgabeModul <Datentyp>Protokoll <Datenverarbeitungssystem>Kartesische KoordinatenThreadBeobachtungsstudieUmwandlungsenthalpiePartielle DifferentiationFramework <Informatik>AdressraumSchnelltasteSkalierbarkeitClientKonditionszahlDatenparallelitätSocketKontextbezogenes SystemMessage-PassingSocket-SchnittstelleMapping <Computergraphik>CodecDienst <Informatik>MusterspracheSoftwareentwicklerEinsComputeranimation
15:49
ProgrammProgrammverifikationFormale GrammatikXMLUML
Transkript: Englisch(automatisch erzeugt)
00:01
Hello, I'm Simon, I'm going to talk about our work on Anaris, a high-order distributed separation logic for modular reasoning about implementations of distributed systems. A distributed system is a system whose components are located on different network computers which communicate and coordinate their actions by passing messages among each
00:21
other in order to achieve a common goal. This communication often happens over a possibly faulty network with message drops and message reorderings, and often follows complex communication patterns or protocols that aren't themselves quite hard to get right, let alone to reason about. The first step is of course to get the general protocol right, but getting an actual implementation
00:44
correct is quite far from trivial. In reality, when distributed algorithms are implemented and deployed, machines can currently run many programs in processes and threads. Each of these potentially participate in different network protocols.
01:00
Some of these programs may even cooperate and communicate locally via shared memory, which adds an additional layer of complexity and makes the programs even harder to reason about in a scalable way. In this work, we define an ML-like higher-order functional programming language, AnarisLang, with higher-order store node-local concurrency and datagram-like network circuits.
01:24
For this language, we define a separation logic, Anaris, for modular reasoning about partial correctness properties of implementations of distributed systems written in AnarisLang. Our logic supports what we call vertical composition. That is, when reasoning about programs within each node, one is able to compose
01:41
proofs of different components to prove correctness of the whole program. For instance, the specification of a verified data structure, for example a concurrent queue or something like that, should suffice for verifying programs written against the data structure, independently of its implementation. Our logic also supports what we call horizontal composition.
02:02
At each node, a verified thread is composable with other verified threads, and similarly a verified node is also composable with other verified nodes, which potentially engage in different protocols. All therianic samples in this work are mechanized on top of the Irish framework and the carproof assistant. So let me start by recalling the ideas of local reasoning from separation logic.
02:25
The most important feature of separation logic is, arguably, how it enables scalable modular reasoning about heap-manipulating programs. Separation logic is a resource logic in the sense that prepositions denote not only facts about the state, but ownership of resources, such as the Pointer Connector that gives
02:42
you exclusive ownership of a particular location. The essential idea is that we can give a local specification to a program involving only the footprint of it, hence the program can be verified without concern for the environment in which it may be executed. These local specifications can then be lifted to more global specifications by framing and
03:03
binding. Here we introduce a separation logic connective called the separating conjunction, here with an asterisk, which holds for a given resource if it can be divided into two disjoint resources, for example the heap. Such that P holds for one and R, in this case, for the other.
03:21
In essence, what the frame rule says is that executing E for which we know a particular whole triple cannot possibly affect parts of the heap that are not separate from its footprint P in this case. The bind rule, moreover, allows us to separately consider expression E and its continuation, here represented by an evaluation context K.
03:43
A preeminent feature of concurrent separation logic is again the support for modular reasoning. In this case, we respect concurrency through thread local reasoning. That is, we can consider threads one at a time and need not reason about interleavings of the threads explicitly. In a way, our frame here includes, in addition to the shared fragments of the heap
04:01
and other resources, the execution of other threads which may be interleaved throughout the execution of the thread being verified. Concurrent separation logics introduce a concept of resource invariance to allow resources to be shared among threads, offering a style of rely-guarantee reasoning. That is, threads may rely on the invariant wholes and access its content, but they
04:22
have to guarantee that it holds at all times. In an aris, we build on these reasoning principles. That is, we are modular with respect to separation logic frames and with respect to node-local threads, but we are also a modular with respect to allowing node-local reasoning about programs.
04:40
To start two nodes, here presented as a triple bar with IPs on both sides, the two IP addresses in which a node should be accessible have to be free, as conveyed by the free IP resources. In turn, the proof of correctness for each node can rely on all ports on that node to be free, here represented by the free-ports resource and the factual P.
05:02
To facilitate modular reasoning about communication, the resources for free ports can be split into disjoint parts. Note here that the node-local post-conditions are simply true, in contrast to the thread-local post-conditions that we saw before, that would carry over to the main threads. In the concurrent setting, shared memory provides reliable communication and synchronization
05:22
between the child threads and the main thread. In the rule-for-parallel composition, that we just saw, the main thread will actually wait for the two child processors to finish. In the distributed setting, however, there are no search guarantees, and nodes are separate entities that cannot be guaranteed so synchronized, as conveyed in this proof rule.
05:42
Similar to how classical concurrent separation logics introduce the concept of resource invariance for expressing the protocols on shared state among multiple threads, we introduce a simple and novel concept of what we call socket protocols for expressing protocols on network communication among the different nodes.
06:01
Here IProp is the type of precision in the NARISH logic. A socket protocol is simply a predicate on incoming messages on that socket. With each socket address, a pair of an IP address and a port, a protocol gets associated, which restricts what can be communicated on that socket. In NARISH, we write a maps to phi to mean that the socket address a is governed
06:24
by the protocol phi. This proposition and resource in itself is duplicable and can be freely shared. Conceptually, the idea is that when a party receives a message and a socket bound to, in this case, the address a, they will acquire ownership of the resources specified
06:40
by the phi predicate. On the other hand, when a party wants to send a message to the address a, they have to provide the resources specified by the predicate phi. So instead of showing a bunch of proof rules, a lot of details about the logic, I want to give you a high-level idea about how one will go about implementing and verifying a simple example in NARISH.
07:03
The example I want to consider is an addition service. It's a simple client and server setup where we have a server that offers to compute sums. That is, the client sends the serialization of two numbers it wants to add, and then return the server response with the sum of the two numbers.
07:22
An implementation in NARISH lang could look like this. This implementation, the server abstracts over some address that it will be communicating on. Starts by allocating a fresh socket and binding the given address to the socket. Now, the listen function here is just a helper function implemented in NARISH lang
07:41
that will keep listening on the socket until the message arrives, and then it will invoke the handler function given as the second argument on the message. The handler function here just deserializes the incoming request into two natural numbers, then it computes the sum and serializes the result. It continues by sending back the result and listening for new incoming requests.
08:05
The client code, on the other hand, in this case, abstracts over the two numbers that it wants to compute on, as well as the server address and its own address. The client, as the server, allocates a fresh socket and binds its address to the socket. Then it serializes the two numbers that it was given as input and sends it to the server.
08:25
In the end, it will just listen for a response from the server, which will be deserializing and returning. So how will we go about verifying this distributed system? So the addition server provides a service, which means that multiple clients that may
08:41
generally be unknown to the server itself may contact it and request this service. What it also means is that primordially, we will have to decide on a socket protocol that describes this service in order for clients to rely on it. So at the level of the logic, messages are records containing information such as its content, sender and destination.
09:03
Here I will use body and from as projection functions for projecting out the content and the sender of the message respectively. So what the socket protocol for the addition server looks like is as follows. So it says that the body of the message should in fact be a serialization of two numbers,
09:20
X and Y. It also says that the sender of the message should be governed by some socket protocol psi, and you have to provide the maps to connective for that protocol. In the end, it also says that this socket protocol should be satisfiable by sending back a message that is in fact the serialization of the sum of the two numbers.
09:42
The last line here uses a magic wand, another separation logic connected, which you may just read as a regular logical implication here. This pattern you see here allows a client to be completely unknown to the server, but it allows for the server to safely respond back in a way such that the client can only rely on what the server actually provides.
10:04
We're now ready to verify our addition service. A specification for the server code could look like this. In the precondition, it says that the socket address provided to the server should be governed by this phi add socket protocol. In addition, the port should be free in that IP address.
10:20
So note that the push condition here can actually be anything, as the narrative logic is a logic for partial correctness, and the server code is actually spinning in a loop here. Let's continue our proof by unfolding the definition of the server code. Let's continue by introducing the two resources in the precondition into our context to the right.
10:41
Let's now symbolically execute the function application. So the next step here is to allocate the socket. In the narrative logic, when allocating a socket, we get a special pointer connective that says that a certain socket handle has been allocated but is unbound. Let's introduce this resource to the context as well and step forward.
11:05
In order to bind a particular socket address to an unbound socket, we have to write the pre-port resource. In this case, we have that already. In return, we get the bound socket handle connective, saying that this socket handle is bound to a particular socket address. Let's introduce this resource as well.
11:23
Technically, we will now continue by loop induction, as the listen function gets called in a loop. However, the essence of this proof is that we can verify the body of the handler function, given that a message is received satisfying the socket protocol. Let's destruct the socket protocol.
11:42
This gives us the psi predicate, two natural numbers, x and y, the maps to connective for psi, as well as this implication that I showed you before. So the socket protocol also gives us that the message received is in fact a serialization of two natural numbers, so we can easily verify the deserialization process. We compute the addition and serialize the result,
12:03
before returning the result to the client. Here, it is not difficult to fulfill the socket protocol, as we are in fact returning back the serialization of the sum of the two numbers, and we finish the server proof. The specification for the client code could look like this. It says that the server address provided to the client
12:22
should be governed by this phi add protocol. Moreover, the client's own address provided should also be free. In the push condition, it says in fact that it does return to some of the two numbers given as input. Let's expand the client code and introduce the two resources. Just as for the server, we can allocate the circuit
12:40
and bind it to the given address. Now we continue by serializing the two numbers. In order to send the request to the server, recall that the server circuit protocol actually requires us to provide the maps to Connective for the sender's own protocol. In this case, this resource can be dynamically allocated.
13:01
We just pick phi client here, exactly as being that the message should in fact be the serialization of the sum of the two numbers. This allows us to verify the message sent. To verify the response from the server, we simply assume that the message received does in fact satisfy the circuit protocol phi client that we just picked.
13:21
This does also give us that the body is actually the serialization of the sum of the two numbers, which allows us to finish the proof. So the addition service example here showcases how we can modularly implement, specify, and verify each component of a distributed system and safely compose all the components, both programs and proofs.
13:42
This exhibits what we call horizontal compositional reasoning. In the paper, we further must show how we can inject a load balancer between multiple clients and multiple servers. The load balancer applies node local concurrency with multiple threads to handle the incoming requests. But most importantly, we use the same specification
14:01
for the servers and the clients as the ones I just showed you. That is, it is actually completely transparent both for programs and proofs that a load balancer is there. This clearly shows the benefits of horizontal compositional reasoning. In the paper, we showcase what we will call vertical compositional reasoning by implementing and verifying
14:22
the two-phase commit protocol as a library functionality. Transparently, on top of this library, we build and verify a simple replicated logging system, where the correctness proof of this logging system only makes use of the specification of the two-phase commit protocol and not its implementation.
14:40
At POPL this year, we presented our implementation, specification, and verification in an ARIS of a causally consistent distributed database. However, we both verified modularly a replicated database implementation, component by component, and we verified client applications in a completely modular way, only relying on an abstract specification of the database.
15:01
You can read much more about this work in the paper or by watching Lian's talk, which can also be found online. So in conclusion, what I've showed you is a programming language and a higher-order distributed separation logic called an ARIS for modular and compositional reasoning about partial correctness properties of implementations of distributed systems.
15:21
By building on top of concurrent separation logic reasoning principles and adding this novel concept of circuit protocols, we offer scalable development and verification of distributed systems through what we call vertical and horizontal compositional reasoning. We also have multiple extensive case studies that showcase our reasoning principles in practice.
15:42
And all the theory and all the examples here are mechanized on top of the ARIS separation logic framework and the Coq proof assistant. Both our paper and our Coq formalizations can be found freely online. Thank you for watching.