9 Replies Latest reply on Dec 1, 2010 9:36 AM by kohei_honda

    Proposed protocol notation changes for Version 2 Milestone 2

    objectiser

      Following a meeting with Kohei, Aybek and Tzu-Chun, we are proposing to make the following changes to the protocol notation for version 2.0.0.M2 of the scribble tools:

       

      1) Import statement

       

      "import" <typesystem> "<typeName>" "as" <alias> ( "," <typeName> as <alias> )* "from" "<location>" ";"

       

      So for example, with Java it would be:

       

      import java "Order" as Order from "org.example.data";

       

      where "Order" is the class name and "org.example.data" is the package (i.e. the location).

       

      For XML, this could be:

       

      import xml "{http://www.example.org/data}Order" as Order from "../schema/Example.xsd";

       

       

      2) Choice

       

      The current choice notation has a problem in that it uses { } curly braces for the overall choice, as well as for each choice path. Through working on various examples, it is felt that the following notation is simpler:

       

      choice from Buyer to Seller {
          Order:
              ...
          op(Cancel):
              ...
      }

       

       

      3) Recursion

       

      With the use of <label>: for the choice paths, it was felt necessary (to avoid parser conflicts and confusion) to change the way recursion labels are defined. So for clarity, it has been made more explicit:

       

      rec Txn {
          Txn;
      }

       

      The way in which the recursion is referenced has also been changed, to remove the previously used '#' prefix.

       


      4) Running a protocol

       

      The way in which parameters (roles initially) are passed (or bound) when running a protocol has been changed. Instead of binding to roles defined within the protocol being run, the roles (and in future other state) are defined as parameters of the protocol. For example,

       

      protocol BuyerSeller(role Buyer, role Seller)

       

      The way in which the protocol parameters are passed can be in two ways:

       

      run BuyerSeller(BuyerRole, SellerRole);    -- so positional parameters

       

      run BuyerSeller(Seller=SellerRole, Buyer=BuyerRole);    -- keyword parameter assignment, as used in the current version

       


      5) Unordered

       

      This is a new construct:

       

      unordered {
          I1;
          I2;
      }

       

      where each statement in the unordered statement can be performed in any order.

       


      6) Try/Catch:

       

      There are no changes to the syntax for the Try/Catch construct. However while we better understand the implications and semantics of this construct, there will be some constraints placed on what can be specified. These will be policed with validation rules.

       

      Initially the constraints will be:

       

      a) Catch interactions must be between same two parties and in the same direction

       

      b) Try block must end with an interaction between the same two parties specified in the catch blocks, and in the same direction, as a way to signify that the 'try' has completed successfullly and that the 'catch' blocks will no longer be triggered.

       

       

       

      If you have any comments on these changes, please let us know.

        • 1. Re: Proposed protocol notation changes for Version 2 Milestone 2
          kohei_honda

          To be sure, this update is also meant for Scribble as a description language, not just for a tool, and will be reflected in its specification document later. Below I list a couple of points that occurred to me, later more.

           

          6) Try-Catch: The main problem is we are not sure about its semantics, in particular endpoint projectability. Hopefully we can follow Sara-Elena-Nobuko's paper:

           

          www.di.unito.it/~capecchi/mpe.pdf

           

          or possibly its generalisation (well, perhaps that may need another investigation).

           

          Other than that, for 5), "unordered" means "the receiver should be ready to get them in either order". So it should follow the same linearity constraint as "par", and in fact *at present* "par" has the same semantics as "unordered".

           

          For 4) role name parametrisation, we hope this gives us a basis for other kinds of parametrisation.

           

          kohei

          • 2. Re: Proposed protocol notation changes for Version 2 Milestone 2
            rawlings

            XML -> XSDL

            import xml "{http://www.example.org/data}Order" as Order from "../schema/Example.xsd";

             

            Assuming that Example.xsd is an XML Schema then XML is not the type system.

             

            1. The W3C's currently prevailing type system for XML is the XPath Data Model (referred to as XDM). This is described clearly in the XPath Formal Semantics. There are prior publications from the W3C such as the Infoset and PSVI, but XDM is currently current by dint of recency.
            2. XML has many other schema languages than XML Schema. If we want to support XML Schema then we should say "xsd" or "xsdl", and not "xml".

             

            I suggest following the W3C's name of "xsdl" and the W3C's definitions of XDM, giving us:

             

            // for XML Schema 1.0 and XML Schema 1.1

            import xsdl "{http://www.example.org/data}Order" as Order from "../schema/Example.xsd";

             

             

            Local Name -> Qualified Name and resource resolution

            As a benchmark let us consider the W3C's own curly braces language notation for importing XML Schema - the XQuery Prolog.

            1. Would Scribble's <location> be a URILiteral? Would the location resolve the XDM way or the Scribble way?
            2. To identify an XML Schema type you'd need more than just its local name, you'd need its qualified name. For example you'd need either "fpml:Order" or "http://www.fpml.org/V5-5:Order". This is made clear in XDM.

             

            Yet not .Net

            Let us consider C#. Would it be the CTS/.Net or C# that was the type system for Scribble's purposes? Surely all that matters is the features used in the .Net Assembly?

             

            The reason I raise this is that other languages targeting the JVM may not be Java, but have the Java type system. This is still a minor concern on Java for now, yet presses hard on .Net from the beginning.

            • 3. Re: Proposed protocol notation changes for Version 2 Milestone 2
              objectiser

              Hi Matthew

              Matthew Rawlings wrote:

               

              XML -> XSDL

              I suggest following the W3C's name of "xsdl" and the W3C's definitions of XDM, giving us:

               

              // for XML Schema 1.0 and XML Schema 1.1

              import xsdl "{http://www.example.org/data}Order" as Order from "../schema/Example.xsd";


              Good point about xml vs xsd - although I think using 'xsd' rather than 'xsdl' would probably be adequate.

               

              Matthew Rawlings wrote:

               

              Local Name -> Qualified Name and resource resolution

              As a benchmark let us consider the W3C's own curly braces language notation for importing XML Schema - the XQuery Prolog.

              1. Would Scribble's <location> be a URILiteral? Would the location resolve the XDM way or the Scribble way?
              2. To identify an XML Schema type you'd need more than just its local name, you'd need its qualified name. For example you'd need either "fpml:Order" or "http://www.fpml.org/V5-5:Order". This is made clear in XDM.

               

               

              The 'location' field would be specific to the type system - so if 'xsd' then the location could be a URILiteral.

               

              In the given example, the XSD type would be identified with the qualified name "{http://www.example.org/data}Order" - using the QName text format. So namespace 'http://www.example.org/data' localpart 'Order'.

               

              Matthew Rawlings wrote:

               

              Yet not .Net

              Let us consider C#. Would it be the CTS/.Net or C# that was the type system for Scribble's purposes? Surely all that matters is the features used in the .Net Assembly?

               

              The reason I raise this is that other languages targeting the JVM may not be Java, but have the Java type system. This is still a minor concern on Java for now, yet presses hard on .Net from the beginning.

               

              Another good point - I think this is something that needs to be decided, however it is not urgent as the typesystem value is just an ID, not a keyword in the language - so it only needs to match the values used by the type resolution system within the tools.

               

               

              Regards

              Gary

              • 4. Re: Proposed protocol notation changes for Version 2 Milestone 2
                perneto
                3) Recursion

                 

                With the use of <label>: for the choice paths, it was felt necessary (to avoid parser conflicts and confusion) to change the way recursion labels are defined. So for clarity, it has been made more explicit:

                 

                rec Txn {
                    Txn;
                }

                 

                The way in which the recursion is referenced has also been changed, to remove the previously used '#' prefix.

                 


                4) Running a protocol

                 

                The way in which parameters (roles initially) are passed (or bound) when running a protocol has been changed. Instead of binding to roles defined within the protocol being run, the roles (and in future other state) are defined as parameters of the protocol. For example,

                 

                protocol BuyerSeller(role Buyer, role Seller)

                 

                The way in which the protocol parameters are passed can be in two ways:

                 

                run BuyerSeller(BuyerRole, SellerRole);    -- so positional parameters

                 

                run BuyerSeller(Seller=SellerRole, Buyer=BuyerRole);    -- keyword parameter assignment, as used in the current version

                 

                 

                I believe it would be useful to unify syntax for "run" and recursion labels. Both constructs are about calling in some previously defined protocol specification; the only difference is whether it's defined in scope or in a separate file/top-level declaration.

                 

                I suggest we drop the "run" and just write

                BuyerSeller(BuyerRole, SellerRole);

                or

                BuyerSeller(Seller=SellerRole, Buyer=BuyerRole);

                 

                 

                5) Unordered

                 

                This is a new construct:

                 

                unordered {
                    I1;
                    I2;
                }

                 

                where each statement in the unordered statement can be performed in any order.

                Have we decided on the projection for the unordered construct? Shall it be still marked unordered in a projection, or just projected in a suitable order, with non-blocking activities first and blocking second? This would ensure parallel execution while still preserving parallel semantics.

                 

                Olivier

                • 5. Re: Proposed protocol notation changes for Version 2 Milestone 2
                  rawlings
                  The 'location' field would be specific to the type system - so if 'xsd' then the location could be a URILiteral.

                   

                  This would make the grammar mildly context sensitive, involving some trade-offs. Do we have any declared principles concerning the design choices, trade-offs, risks and sensitivities of the concrete syntax? Some principles would avoid a case by case decision on the language design.

                   

                  If I were to characterise aspects of the concrete syntax, it would be: lexically akin to C++, and parsed akin to Haskell. Some such aphorism will lead the project.

                   

                  I suggest distributing the snippet of the ANTLR grammar being changed, with the change to it, to facilitate these discussions.

                  • 6. Re: Proposed protocol notation changes for Version 2 Milestone 2
                    objectiser

                    Hi Matthew

                     

                    No unfortunately we don't have choices/trade-offs/risks/sensitivities documented for the concrete syntax. Primarily the syntax has been driven based on theory we intend to use, and then finding an appropriate textual notation for those constructs. Not sure if Kohei has any other guiding principles when considering suitable constructs/syntax?

                     

                    The changes to the ANTLR grammer for the recent import change was:

                     

                    http://fisheye.jboss.org/browse/scribble/development/java/trunk/bundles/org.scribble.protocol.parser/src/main/antlr3/org/scribble/protocol/parser/antlr/ScribbleProtocol.g?r2=391&r1=384

                     

                    The type system is simply an ID, and the concrete type and location fields are string literals.

                     

                    The other changes can be tracked here:

                     

                    http://fisheye.jboss.org/changelog/scribble/development/java/trunk/bundles/org.scribble.protocol.parser/src/main/antlr3/org/scribble/protocol/parser/antlr/ScribbleProtocol.g

                    • 7. Re: Proposed protocol notation changes for Version 2 Milestone 2
                      objectiser

                      Hi Olivier

                       

                      I agree that the inline run, and recursion constructs, are looking more and more the same - with the benefit of the inline run being that parameters can be bound - which is probably a limitation of the current recursion construct.

                       

                      I think we need to experiment with some examples.

                       

                      Olivier Pernet wrote:


                      Have we decided on the projection for the unordered construct? Shall it be still marked unordered in a projection, or just projected in a suitable order, with non-blocking activities first and blocking second? This would ensure parallel execution while still preserving parallel semantics.

                       

                      At the moment I am projecting it as an unordered construct. I think the comparison of sequence and unordered constructs will be relevant when doing conformance checking between two models - i.e. where one uses unordered and the other sequential (or a mixture). But for projection itself, and I think we just keep this simple between the global and local models.

                      • 8. Re: Proposed protocol notation changes for Version 2 Milestone 2
                        kohei_honda

                        About the recursion:

                         


                        I believe it would be useful to unify syntax for "run" and recursion labels. Both constructs are about calling in some previously defined protocol specification; the only difference is whether it's defined in scope or in a separate file/top-level declaration.

                         

                         

                         

                         

                        I suggest we drop the "run" and just write

                        BuyerSeller(BuyerRole, SellerRole);

                        or

                        BuyerSeller(Seller=SellerRole, Buyer=BuyerRole);

                         

                        This is a interesting thought, and also let us think about recursion.  A summary of my view is:

                         

                        (1) This may result in economical descriptions in some cases.

                         

                        (2) On the other hand,  It may also force designers to describe additional data (roles etc.) when doing recursion, though this may be avoided by some means: but such different treatments of protocols can be confusing.

                         

                        (3) As another point, it  may become a bit complicated in mind whether we are using  something external or "going back" to something. 

                         

                        (4)  The keyword "run" is not so good since it looks like we are calling something dynamically even if it means we are just having a conversation following a protocol which is nested at that place, though it is not too inappropriate.

                         

                        (5) "run" can mean two things: it is a macro, so we are not having a nested conversation;  or we are indeed having a sub-conversation. The fact is, we have not studied the theory of nested conversations yet --- I am hoping Tzu-Chun's thesis can treat it from the viewpoint of monitoring, but it also has a significant programming consequence.

                         

                        (6) A recursion as we see here is a recursive types as applied to (sort of) imperative programs. As such, it is an interesting question what way is best for their corresponding programming constructs.

                         

                        Generally, I think we need to think about this in more detail.

                         

                        About unordered:

                         

                        5) Unordered

                         

                        This is a new construct:

                         

                        unordered {
                            I1;
                            I2;
                        }

                         

                        where each statement in the unordered statement can be performed in any order.

                        Have we decided on the projection for the unordered construct? Shall it be still marked unordered in a projection, or just projected in a suitable order, with non-blocking activities first and blocking second? This would ensure parallel execution while still preserving parallel semantics.

                         

                         

                        This is also a good point. I believe we have it in effect, but not yet completely enunciated. It is basically *Par* at present (as far as *par* does not force us to be really in parallel). Three points:

                         

                        (1) EPP is doable I believe following par.

                        (2) type checking can be a bit interesting.

                        (3) monitoring is doable.

                         

                        All these points need be clarified. Let's do it. This may be a good practice for the theory of MPST, and moreover essential for Scribble. And can be an interesting sub-topic for a paper, indeed.

                         

                        kohei

                        • 9. Re: Proposed protocol notation changes for Version 2 Milestone 2
                          kohei_honda

                          As to Matthew's question:

                           

                          This would make the grammar mildly context sensitive, involving some trade-offs. Do we have any declared principles concerning the design choices, trade-offs, risks and sensitivities of the concrete syntax? Some principles would avoid a case by case decision on the language design.

                           

                           

                          When we discuss each construct, we do carry out extensive discussions on the trade-offs. Before we were taking pictures, but this time we discussed many things very fast so we could not take any, and our memory is fading.

                           

                          A set of fundamental guidelines indeed exist, from a theory viewpoint --- or from a safety assurance viewpoint. From this viewpoint we may say the following are the guiding principles:

                           

                          (1) Endpoint projectability
                          (2) Runtime monitorabiility
                          (3) Static checkability

                           

                          Each needs be carried out by an efficient algorithm, especially (1) and (2).

                           

                          (1) tells us the semantics of the description. (2) is essential even if we do not program with sessions (conversations). (3) becomes important when we do program with session types.

                           

                          Beyond them, we shall have such principles as:

                           

                          (a) Orthogonality (record types and tagged unions)

                          (b) Complementarity (while and do-while, similar but serves differently, and convenient)

                          (c) Elegance, simplicity

                          (d) A bit of care for convention

                          (e) Sheer expressiveness

                           

                          We assume as given such basic properties as ease and uniqueness in parsing, etc.

                           

                          Other than these, I hope that, in this forum, we can mature our shared understanding on how we may value language constructs, what viewpoints we can have, and how we think about their trade-offs.

                           

                          kohei