“Multiparty Session Types and their Applications to Concurrent & Dist. Systems” by Nobuko Yoshida

So first I want to introduce you to our website, on the main website on here if you want to read or test our theory based on the session types, and the order of information, more or less, will appear here and we have a home, and there are either some news under — our work was announced by active developer in the conference on Scala Some of the session work that is applied to that Scala language, and we have application to Go where we talked about our work at the Golang UK conference with developers, and like this, we have some information listed here

And then we have the home and then all publications are listed here, and so I will select some of them to talk with you — to talk today, and about the other things that we have here And, also, tools, we have several applications with the session types to Go, and Scala, and Haskell, and for example, you have C++, and the main project is with Redhat, Cognizant, and OOI with Scribble projects, of which I will talk about, and actors in the Python C, and the Java and so on there, and those are the tools under public source code available from git which you can get And I want to inform you about one thing, and Kohei Honda was my collaborator and he originated in session types and his information is also available here, but I want to start now about the talk from here So what is a session type and session types is the types, you know types, for example, Boolean, Integer, and Character, and also bit, which is difficult array types and in Haskell, you have functional types, session types is a types likes functional types for concurrency and method parsing Today, I introduce you about session types and so that everybody here can understand session types definitely definitely yes

I promise you [laughter] And so here you go And here is the current members of our group I have three female PhD

students, who’s female students coming next year: And also another postdoc and this is a selected list of our publications, I don’t know why it’s not displayed properly [fixing display] OK, this way it’s better And so I’m not talking on everything today, and this is two years of our publications, but, so I cut out my publications and there are three categories I can find: These types are a very theoretical work of the session types and session types is the type theory of concurrency, so these papers are very difficult, probably, for you to read and very complicated However, green letters is about applications of session types to the programming language, such as MPI, MPI code generation and verification, and Haskell and Java API generations, and applications to the Go language and the Scala, and we have wide, disparate applications with the session types so that you can see it’s very easy to integrate into the programming language So after this talk, I want to hear your opinion what is the maybe the application with that session types to your problem And so, I also selected what you can read among all the best publications not only by me, but also of the team, and I selected separate papers from theoretical, and binary and multiparity session types and I talk about Scribble description language and also about the last talk which is about monitoring of protocols Actually I’m also talking about the monitoring protocol and I will talk about it, and also if — if I have time, I will talk about the code generations, and how you can apply the automata theory and linking with session types to analyze the Go language by Google end to end >> So let’s start! So five session types Now currently, computation of concurrency and the communication is ubiquitous, and you can find the way to organize software is increasingly based on communication, for example, cloud and the microservice and the message passing protocol, network protocol previous one is also best under communications

So questions here is how you can formally describe, implement control, communication, you said communication, interaction, but they are not divisible, but how you can formalize it, and reason it, and how to apply and there is a past theory of mobile process developed, particularly in the European theory, and can be applied to real distributed application and programming language And these are the questions we are trying to answer in our community So this talk I will show how to manage multiparty session types can be applied to verifying large-scale cyber infrastructure for E-science in US I am I’m going to show you how this project – Ocean Laboratory Initiative project and this was run 5 years, historically, and this Ocean Observatories Initiative is still running You can find the web page but the core project, developmental project, finished a couple of years ago, and we participated and applied the session types to verify this cyber infrastructure, which I want to a bit talk about now

And so this is a very big project and very expensive project, but the aim of this project is extremely simple So you get to that real time sensor data constantly coming from both offshore and onshore and using bouey, submarines, and cameras, and satellites, and transmit this data using high-speed networks, so that various things and the university can use this data to analyze immediately And why it is interesting to observe the oceans, because this earth is 70% are oceans, and they are a very, very active source of information For example, not only just temperatures, but also bacteria, and circularity, and circularity, and also the sun and dust and the wind All of this information very useful to get to it so that you can use to analyze for example, for example, to predict the forecasts and predict global warming and also predict earthquake — so getting analyzing this data immediately, it’s very important And so, so that’s these things, and so this is a big picture of the Ocean Observatories Initiative and getting sensor data and from our seas and transmit these data using very big cyberinfrastructure, so that they can develop scientific projects, and realtime and remote controlling and things like this and, this is a view of that cyber infrastructure, and interestingly — the interesting point of this project is that they build this cyber infrastructure from scratch using methods with middleware, such as I worked with the people and so what you can observe here is that there are loads of loads of message-passing, and because you need to transfer the messages from point to point, and so that they’re use case is basically best with message-passing Here we have the questions: How you can catalog, manage, describe, control, and verify this message passing That is reason why I work with these people using the theory of multiparty session types So why multiparty message passing protocol is important because we want to assure the correctness of the message passing For example, this cyberinfrastructure, you needed to control the order of the messages and the synchronization, and you want to guaruntee messages are robust and not and not circular, so for example, deadlock freedom and liveness and also this cyberinfrastructure, it’s too big to verify statically, so you need to do something dynamic analysis, and monitoring, discovery, also maybe you want to control the message logically, for example, using information with the timers

So why did oceanography people interested in the theory and this fundamental work and work with us? Their cyberinfrastructure is very expensive, so that it was assumed it would retain 30 years, so if we retain 30 years, you want it to build the correct infrastructure, that is the reason we are working with them, and the part of that project So why multi-party session types? But I want to say why type best verification is important? So Robin Milner is one of the two Turing winners in the UK and he — he initiated ML — functional programming and also he created ccs, process calculus >> And he said why types are important is that types can digest the computations, so as I will explain, session types can describe the communication protocol types, and why types are important is that you can combine the notion of types through programming language and through the chain easily, as you know, with Java and Haskell and Python Python is not a typed language, but these kind of things can be easily integrated to — to the change Another thing is that types are very cheap comparing, for example the approach of model checking, because normally it is finished by linear type checking is finished compiled under linear type or polynomial type, and session types most of their verifications, are polynomial types, and also it is easy to extend, for example logical verification, even dynamic monitoring, which I will explain now And before that, I really think, and this is ideally, I ask you to also communicate with academic people, because I believe that dialog between industry and academia are extremely important, also discover the very theoretical fundamental discovery, and the reason is that multiparty session types was discovered by the interaction with industry people, which I want to explain in a bit of detail So session types, it’s starts at the type theory of the mobile process, actually quite a long time ago, ’98, and at that time, nobody used it

Just a theory of the mobile process But after that, whoever saw this coming and the people tried to control or verify web service language, and so Milner, Honda and I are invited to join W3C working group, one working group called choreography description language group And where we proposed to use session types However, their language, standardization language was very, very complicated, so that we spent five years to formalize the idea, because we didn’t understand what they are doing [laughter] And so Kohei it was a bit; (he) initiated this project, and then he invited a couple of industry people, and then they started a venture company called Pifortec, and we started a simplification of their language called Scribble And that is the original multiparty session types

But what I want to show is that These is the original CDL language and you know where industry people meet and discussed about the standardization, it becomes extremely complicated and this is a protocol of Hello world But, you don’t understand that this the protocol of Hello world! Because they want to put for example, roleType, participantType, channelType and so on And so it’s quite complicated And so Kohei sent — Kohei — sent quite a bit of emails to a couple of industry partners Let’s forget the CDL and start from scratch to write a very simple protocol language called scribble, and that is the start of that multiparty session type theory, actually, and so this Scribble language, I will introduce later, and everybody understands this is hello world protocol

And so here is that protocol declaration, and the keywords and the hello world, and they are two persons — You and World And we send a message hello from you to world And this is the type to describe the global protocol And so after that, actually, I went to show and also I’m going to show, how binary session types, it’s extended to the multiparty session types, but very long time ago, we couldn’t extend and we don’t know how to extend to theory of binary session types to multiparty session types, but using the idea with the Scribble with CDL, we could actually extend to the multiparty session types and so we wrote the paper that accepted at POPL, top-tier conference of the programming language and we had quite a benefit of that engineering idea So we are always welcome to getting the idea, and also, because theoretically extended and Scribble is promoted at one at the later group projects after that And we started to work with several industry people and also currently expanding this circle

So now I want to show what are the session types, and actually I hope everybody here understands at least the binary session types, because the idea is very simple And binary means two-party session types, OK? So, let’s think this is online shopping, and there are two participants, or roles, buyer and seller And the buyer tried to buy a book from the seller, for example, Amazon, sending that message title, under this type, and then seller sends back the quote to the buyer, and then there are two choices OK, or quit, and if we click OK, and the buyer sends an address, and then the seller sends us the variable date, and otherwise, if he doesn’t like that quote, he quits the protocol OK? Everybody understand? And basically send and receive, and there is a choice, and then if choice, one choice, will continue, otherwise quit that protocol

And so these session types from the buyer’s viewpoint, written like this, OK? So up means !, ! means output Output to string, and input is a quote, and this plus mark means there’s two choices OK or quit If OK, send us the link and get us the date and end the protocol, OK? And then quit, end the protocol So there are your choices here, OK? So that if you can write a UML diagram nearly using the session types

Next, and then now you get to the idea Interesting thing is that seller session type is the dual What do we mean dual? Dual is swapping output to input, input to output So ! means output, input means question So this is the viewpoint from the seller and the buyer, and this ampersand, it’s waiting a choice, so he is awaiting the choice, OK, or quit And once you type that program, using the session types and the buyer and the seller, you can see there is no deadlock, because input match output, output matches input and there is a choice always then waiting a choice, OK? In this way, you can guaruntee deadlock freedom using the session types, just checking the duality, and this comes along — the underlying idea comes from linear logic by Girard and that is an important point of the session types

Now, these are the two players, two people, but how you can extend to that managed parties? So, there are three parties here, and I just extended this scenario to that another buyer, and now scenario is that you tried to buy — two buyers tried to collaborate with each other on sending a message and buy the book, and now, protocol becomes a managed party, and so seller, first the buyer sends a title and the seller distributes the quote, both buyer 1 and buyer 2, and buyer 1 sends that quote, how much he can contribute to the buyer 2, and then there is another choice repeating like this, OK? However, how you can manage deadlock free with more than two parties? The idea is not so simple, because you may think, this is like let’s divide the binary– — into binary in this managed party protocol That doesn’t work Why it doesn’t work? Because you need three separate session types, and previously, because you have three combinations: buyer, seller, buyer 2 Ok? And all protocol becomes split And not only this protocol

Then this protocol becomes a type of if we use binary session types, but what we want to prove is that describe and check with this multiparty session types, how you can do it using the idea of the session types And here it’s a bit technical and faster So the idea comes from the choreography description language and as I told you before, and first of all you need to write the global protocol because you wanted to give that protocol For example, if there are Alice, Bob, and Carol, and this role, and this type of T1 message to B, B to C, and then C sends to A You just described this as a type like this, and this examples of the choreography protocol, like A send to B, B send to C, C sends to A like this

This is a type which you need to describe first And then next step is that You need to then this to project into the binary session types, so that each endpoint can have the interface with output and input and the choice so if you implemented the program following this sequence, then each people interact correctly And, but this is a projected, because I would be able to throw down, supported from the viewpoint of A A sends the type of message, T1, to B, and which means send B type over T1, and C sends the message T3, to this person, and annotated by this participant, who am I going to send, and from whom you are going to receive

So A has a data type B has this type, C has this type Because these three are projected from these global types, and once you get to these types, each participant behaves correctly, so that you can guarantee deadlock freedom, Ok? However This is a bit difficult So maybe it’s a bit difficult to explain, but if you do not follow these global types, this is the bad local type which does not follow this projection, but this is a dual with each other but you can see that more people are waiting and, even dual with each other, so that this is a deadlock

So writing global types and the project does work to check the endpoint protocol So now I’m going back to the sea again, and this this is the ocean observatory initiative institution, and in front of the sea, because they like sea, and this is the pier by University of San Diego, I think, and they started the oceanography first in the world, and this is the storage which stores the instruments and we feed with them and worked with them and they developed some architecture with their developers And this is my student, and this is my post doc who developed their protocol And so this work, and so — [laughter] I want to use these global types and the global type is

these multiparty session types are used in various ways and I only introduce one way today at the main applications, and the rest I will quickly explain today I hope I have time to manage it So first of all, global type, its projected to local types, but these local types looks like the state machine, and using this information we write a program for example Alice, Bob, Carol, and check incoming and outgoing messages correct against these local types That is the application I will explain

And before that, I want to briefly explain about what is Scribble language, and Scribble language is the — Scribble language — is a kind of programming language to describe that multiparty session types, and as I said session types start from the types of the theory, of the concurrency, where we write all these papers with Greek-letters and then industry partner said that they don’t want to read Greek-letters paper and they want to read this kind of notations, so we developed this protocol in the description language with them, and they designed them, and then automatically you can — you can project to it, but before — because I don’t have time, I really want to quickly show what is that application here, and so, this is a protocol we try to specify from the Ocean Observatories Initiative Project: I show here And so this is the Scribble web page If you are interested after my talk, because it is quite a big project that I will explain later And this is web page that you can test Scribble protocol and then you can check under whether this is correct, and you can project this is automatically like this, so this is a bit of an education tool

So what I want to show today is how we try to verify that using the session types architecture, this protocol between the customer agent and the provider agent, and interactions specification of the ocean observatory, and so as you can see, the developer wrote about this kind of UML diagram It is very complicated and it is very ambiguous, and it is not clear what they want to do with this kind of — on the natural language explanation, so what we did is that we that actually tried to write down, and before that, I want to show a bit monitor architecture of this OOI and the what they do is that they analyze and control this kind of message passing, and using various kinds of hierarchical architectures, and you can see how Scribble is located at the bottom part: And they can intercept in the various sophisticated policies and sent out with that architecture and decide to–sorry–whether you can throw away and the message that is orchestrated, finally, can control whether you can throw away messages or not This is the way that you can integrate a lot of different tools and ideas That was part of the Ocean Observatories Initiative Tool But before that, I want to go back to our stuff

And so, if you use that session types, you can write this kind of ambiguous protocol very clearly and first of all, you declare this is a multiparty protocol Actually only two roles, but negotiate role communicator as C Role producer as P And C and P are abbreviations Next, we can write that C gets a message and that this is a submessage and operations is a propose can be sent from C to P and there is a choice after P, and then for example, accept and confirm, or reject, and propose are like this

You can add these kind of things and then choice can be nested and also you can not understand probably the declaration, but there is the causation of this protocol so that you can choose stop or because of the protocol, you can try and try many times like this And the next step is that two you can automatically project the global type to local type by checking the global type is correct, and this is that projection from the viewpoint of consumer, and the basically just chop that view of the global types to the local types And then you generate the state machine, and so this is that corresponding, this corresponding with these local types and so that you can check that incoming and outcoming messages correct against this state machine And this is Scribble and the web page, and I show it and we have a GitHub and various source files can be get from here, and we have several applications based on this, but probably I’m not sure how much time I have remaining, but let’s see And this is the big thing of the OOI so that we can finally control all of these kind of things by underwater vehicles and this is the pictures, and so I’m — this is that interface of the OOI so you can get this message constantly So I want to show the demo of that monitoring, how you use the Scribble to monitor the message and very quickly to two minutes

[prepping demo] So this is an RPC protocol in between the Scribble language and this is the Python code, endpoint code, you want to monitor in it and you can see that there is something like — sorry — I think it’s better if I stop it its a bit quick So this is the that global protocol which tries to describe the interaction with the provider and the requester and first you needed to write this kind of protocol which you want to monitor And then this is a Python code which you want to monitor and whether they correctly behave or not And you can see several other operations such as accept and reject, and invite We want to check whether the message is correct or not

And this is some kind of wrapper and Hello client and now we tried to run the batch machine of the OOI, and so first you needed to execute the tool and batch machine, and then Python monitoring, inside this capability [running demo] over here [running demo] [running demo] And then so now we have hello client, and so, then, now you can see message is correct monitor or not, and returns a status, such as correct, and correct, and correct, and you can correct message input and output and now you change this correct program to the wrong incorrect program, changing accept to invite, and then then monitor again And the first one is correct and then you can show the next message is incorrect like this, and like this by monitoring the message against the Scribble, you can guarantee that you can detect the bad message, and protocol and this is quite a simple application for that session test Like this, we worked with the OOI people And, I’m showing this — sorry, where are it going? [prepping video demo] And so, I show only one application on dynamic monitoring, but this general idea of global protocol and this projection can be applied to various different applications which I want to show a bit quickly, and I show the dynamic monitoring, and also, you can of course use the session types by type-checking, using the session types as types, and write some programs such as Haskell and do the type-checking integrated session types and so and so on that you can guarantee that it will involve many participants

Also, interesting application is that you can generate the code for that global types, and for this we have two works of the MPI code generation and Java code generation Probably, I cannot do the demo, because I have a shortage of time today, and so also, you may think the other way around, not writing global type, but generating global types from the communication of the program, may be useful Actually, we have the work of this, and we applied this to two different applications which I just want to very quickly show, and this slide I’ll skip And basically session types have mathematical correspondence with communicating automata I don’t know if you know the communicating automata, but automata which can describe input and output and asynchronous messages and I was very shocked, these entity I discovered in very old literature of the communicating automata, which exactly corresponds with that of binary session types

And the communicating automata is that basically it is very powerful and it is undecidable to check whether this communication is deadlock-free or not, but if you restrict that, this communicating automata, with certain kinds of conditions, which exactly similar with the session types, deadlock-detection becomes decidable and actually this was proved before the session types appeared, so that mathematically good structure arrived in the different areas, That was one surprise thing when you do this kind of research work And, so on this I may skip a bit Interestingly we applied this this approach to this legacy code analysis of a bank application, but I will skip it And I want to show one example of how you can build the session types from the communicating automata, so there are — so natural question is whether you can extend binary approach to the multiparty approach? And the right-hand side is the communicating automata, and you cannot see how they interact, but you can imagine this kind of flow of the message, it’s analyzed by the source code, for example, Java or something, and then you can get to this automata, but you don’t know how they interact correctly or deadlock-free, but we could build the session types by using a certain kind of theory and decidable and then you can check whether this automata for party interaction is correctly globally organized and then translated into that BPMN choreography language This is just a couple of applications and I just want to show one quick application to the

Go language by Google And I don’t know if you know — oh, maybe it’s better to show that a little bit fast [prepping video] I guess many of you know that Go programming language by Google, which is based on the process calculus such as Csp and pi-calculus, basicallly they are based on message passing and channel communications, and it is written here and their communication is basically — they encourage to use message-passing instead of shared communications

And we applied this approach to analyze deadlock detection and I have five minutes, so that I will show the demo here [opening demo] So, this is the Go interpreter, and this is Go programming language You can see send and receive work and so this is — this describes that basically Sorry, it’s made too quick And, This is the deadlock, because send and receive are mismatching, and if you run this program by Go interpreter, you can see send-to, and receive-one, so it is obviously deadlock

And, then, actually Go has a runtime deadlock checker So you cannot write, because they detected a deadlock, but their deadlock analysis is first of all dynamic, and cannot capture that partial deadlock, and we tried to solve this using the synthesis of the session types And now we change the protocol just using the while loop like this, and then this is a still a mismatch of course — protocol And working, working, working, which means that because each Go routine that’s running, they’re deadlock (analysis) dynamic tool cannot capture this deadlock, OK? So now we are trying to use our Go tool which generates the automata from each Go routine and build a global type so that you can check whether the Go language or Go program is a deadlock-free or not by static analysis And so first we create the state machine, from each Go routine and with this we can show that first of all and, like this, You can create just a state machine from each Go routine code, and then use synthesis to try to find out the matching between input and output, and using our session types theories

And so we check it [checking] and generate it, and then here I can say — sorry — I can say here we said this checking it’s incorrect, because it doesn’t — input and output — doesn’t match, and it is not also well-formed So what you can describe visually in the session type is that , because you can generate from these kind of global types, using the session type theory, and you can see there are two ends which is incorrect global types So this shows a deadlock I cannot explain details with this time And now we change the correct program, only we have send and one receive and then now we do the same things, and generate and check now, whether they are compatible or not using the this — our automata theory, and then it returns correct now? I think so

OK And since its check is true and now we can build this tool using the dot applications, and now because we see that this interaction is correct, like this And so I wanted to show another real code generation example, which applied to Scribble to Java directly, but probably I don’t have time now? And so maybe I should probably stop, or I can just quickly show it >> ZEESHAN:

>> Can I do, or maybe better to have questions? >> ZEESHAN: Yeah >> Yes, OK, OK, because it’s probably better to — and so, anyway, so I will finish my talk here, and every information that I said, you can see from the web page, but it’s quite probably difficult to understand what tools and papers you should read, and it also depends on interest, you know, if you want to use the session types to verify and specify the message passing, and you are very welcome to directly send an email to me and so that we can start a really good collaboration and thank you very much [applause] >> ZEESHAN: We have time for a couple of questions and then head out for lunch >> So, you mentioned that one of the benefits of using session types compared to model checking in like CCS or pi-calculus or CSP is that you don’t have the same kind of (state) space explosion that you would if you were doing model checking in a process calculus

Do you have any intuition for sort of like where that boundary is? Where the model checking approach isn’t going to be as useful because for a lot of the examples that you presented, I think you could do the same kind of static analysis and produce something in one of these process calcules — calculus — calculi — and run them through a model checker, and sorta do the same kinda of checks, and so I would be interested to hear if you have a sort of have an idea of sorta where that becomes untenable, where you sorta have to do this type-based approach instead? >> Nobuko:Yes, yes, so we actually have the publication to to the TACAS this year on linked model checking and session types and we used a model checker and also a session type checker to run the benchmark, which is good And also, an automata approach, in TACAS 2016, so this year’s TACAS paper and compare Actually some kind of checking, you can use model checking and some of the examples, model checking scales very well, because, now, it is out of bounds, but certain kinds of normal kinds of session types structure between the program language, still type-checking scales much faster than this, and this is really depends on the examples And actually, I said generally, you know, session types scale well, but complicated examples, and because of the effort of model checking people, it may run sometimes faster for big examples Actually there are many interesting big examples

And so, Golang, we have our next work, which we used — actually — more like symbolic semantics, because session types are too limited So, there are various links of the types of the pi-calculus and the session types, and so, this is a really good question Thank you Yes >> ZEESHAN: Any other questions? All right, thank you, that’s good

[applause]