Scribble Language Reference
|
This document is the Scribble language reference. It defines the language syntax and conventions for Scribble protocols. It also defines the semantics of Scribble protocols in terms of event traces.
Scribble syntax is specified using a BNF-like notation. Terminal symbols are in purple with typewriter font. Non-terminal symbols are in italic. Each grammar rule starts with a non-terminal (the name defined by the rule) and ::=. Parentheses ( ) are used for grouping grammar elements, square brackets [ ] for an optional element, vertical bar | for separating alternatives, star * for zero or more repetitions of the preceding element, and plus + for one or more repetitions. An ellipsis is used for choice of any single character from an inclusive range of ASCII characters, e.g. a … z means any lower case letter.
This document uses the following terminology related to Scribble protocols.
This section specifies the lexical structure of the Scribble language.
White space is defined as the ASCII space and horizontal tab characters, and line terminators (ASCII LF, CR or CRLF). White space in Scribble protocols serves only to delimit lexical tokens.
Block comments are opened by /* and closed by */. Single-line comments start from // and end at the first line terminator. Comments do not nest. Block comments have no special meaning within a single-line comment and vice versa. Comments delimit lexical tokens similarly to white space.
An identifier is a sequence of ASCII letters, digits and the _ character that does not start with a digit. Identifiers cannot be among the reserved keywords. Identifiers should not be longer than 256 characters.
The following character sequences are reserved as Scribble keywords. They cannot be used as identifiers or message operators.
|
This chapter specifies the syntax of the Scribble language.
The Scribble package hierarchy is a tree of package nodes. Scribble source files are represented in the hierarchy as special package nodes called modules, and occupy leaf node positions in the tree. Non-leaf nodes (and leaf nodes that are not modules) are simply called packages. The non-leaf nodes may contain other packages and modules as subpackages. Packages correspond to directories on the file system, with subpackages nested inside their parent package directories.
package-name ::= ( identifier . )* identifier
Every package has a simple package name and a fully qualified package name. The simple package name is an identifier. The fully qualified package name (package-name) is a dot-separated sequence of simple package names, where each identifier in the sequence denotes a package that is a direct subpackage of the preceding package, starting from the root package and ending with its simple package name. The above terms may be adapted to simple module name and fully qualified module name with the same meanings when referring specifically to a module.
A Scribble module is a leaf package. A module is a text file with four parts: a package declaration, an optional list of import declarations, a list of zero or more payload type declarations, and a list of zero or more protocol declarations. The start symbol of the grammar for the contents of a Scribble module is module:
module ::= package-decl ( import-decl )* ( payload-type-decl )* ( protocol-decl )*
A module starts with a package declaration that specifies the fully qualified package name of the module.
package-decl ::= package package-name ;
The filename of the module is required to be the simple package name appended with the suffix .spr.
import-decl ::= import package-name ;
In a module import, the package-name specifies the fully qualified package name of the module to import. Therefore, the package-name indicates where, in the directory structure, the module file that should be imported is located.
The members of a module are the payload types and protocols declared in the module. Like packages, module members have simple member names and fully qualified member names. The simple member names of payload types and protocols are declared by the corresponding payload type and protocol declarations. The fully qualified member names are given by the fully qualified package name of the module to which the member belongs, appended with a dot (.) and the simple member name.
The payload types and protocols that are visible within a module are:
A payload type represents the data carried as a payload by a Scribble message.
payload-type-decl ::= type < identifier > "extidentifier" from "extidentifier" as identifier ;
Payload types are declared by the keyword type. The format of the payload type is specified by the schema type identifier in the angle brackets. This is followed by the first extidentifier specifying the name of the type defined in an external message schema file. The second extidentifier specifies the filename of the schema source file that provides the definition of the payload type. The final identifier specifies the alias by which the payload type should be referred to within the current module.
When a payload type is declared, the specified source file is searched for on the Scribble payload type path. The payload type path is searched in order and uses the first match that it finds. A terminal error has occurred if the file is unable to be found.
The payload types that are visible within a module are the declared payload types when referred to by their aliases.
A Scribble message signature comprises an operator header and an optional comma-separated list of payload types.
message-operator ::= ( letter | digit | _ )* message-signature ::= message-operator ( [ payload-type ( , payload-type )* ] ) payload-type ::= [ identifier : ] identifier
A message operator is a (possibly empty) sequence of letters, digits and the ASCII underscore character. An operator cannot be among the reserved keywords. The payload of the message is specified by the optional group inside the parentheses. The optional identifier in a payload type is a annotation that associates a variable name to the payload. If present, the annotation is followed by a colon. The mandatory identifier is the data type of the payload. The data type must be a visible payload type.
A protocol declaration is either a global protocol declaration or a local protocol declaration.
A global protocol declaration has the following syntax.
global-protocol-decl ::= global protocol identifier global-protocol-definition global-protocol-definition ::= [ < parameter-list > ] ( role-list ) global-interaction-block | ( role-list ) instantiates identifier [ < argument-list > ] ; role-list ::= role role-name ( , role role-name )* role-name ::= identifier parameter-list ::= sig identifier ( , sig identifier )* argument-list ::= message-signature ( , message-signature )*
A global protocol declaration starts with the keywords global protocol. It is followed by a name for the protocol, a role list and an optional parameter list. A role list is a comma-separated list of identifiers each preceded by the keyword role. A parameter list is a comma-separated list of identifiers each preceded by the keyword sig (this sig specifies the kind of entities we are abstracting, here meaning a message signature: other kinds such as payload types may be included in later versions).
The global protocol declaration then either ends with a global interaction block, or the instantiates keyword followed by an identifier. The identifier in the latter case specifies the name of the parent global protocol being instantiated.
The body of a global protocol declaration is a global interaction block. A global interaction block is a global interaction sequence enclosed by curly braces { }.
A global interaction sequence is a possibly empty sequence of global interactions: point-to-point message transfer, choice, parallel, recursion and continue.
A point-to-point message transfer specifies the communication of a single message between two roles.
global-message-transfer ::= ( message-signature | identifier ) from role-name to role-name ;
A message transfer starts with a message-signature or an identifier declared as a generic message parameter. The role-name immediately after the from keyword specifies the sender of the message. The role-name after the to keyword specifies the receiver.
The choice construct specifies that one role chooses one out of a set of interaction blocks for the protocol to follow. The choice of an interaction block is mutually exclusive; the conversation follows exactly one interaction block.
global-choice ::= choice at role-name global-interaction-block ( or global-interaction-block )*
A choice starts with the keywords choice at, followed by a role-name designating the role responsible for the choice. This is followed by a list of global interaction blocks separated by the keyword or. The interaction block list cannot be empty.
The parallel construct specifies a set of interactions that can happen concurrently.
global-parallel ::= par global-interaction-block ( and global-interaction-block )*
A parallel starts with the keyword par, followed by a list of global interaction blocks separated by the keyword and. The interaction block list cannot be empty.
The recursion construct is used to specify loops in the control flow of a protocol.
global-recursion ::= rec identifier global-interaction-block global-continue ::= continue identifier ;
A recursion point is specified by the keyword rec and an identifier label for this point. Within the following global interaction block, the keyword continue followed by a recursion point identifier specifes that the control flow of the protocol should return to that point.
The interruptible construct specifies a sequence of interactions that may be interrupted by the specified roles. A raised interrupt is communicated to all other roles in the conversation. On raising or receiving an interrupt, the role exits the interruptible block, activating the subsequent action(s). In the present version, this means the endpoint will exit the conversation.
global-interruptible ::= interruptible global-interaction-block with { ( global-interrupt )+ } global-interrupt ::= message-signature (, message-signature )* by role-name ( , role-name )* ;
An interruptible starts with the keyword interruptible followed by a global interaction block. This is followed by a list of the keyword with, each followed by a message signature and a global interaction block.
The do construct specifies that the interactions specified by another protocol (called the target protocol) should be performed inline with the current conversation. Note that the Scribble do construct should not be confused with do statements found in other languages, such as for performing loops or for performing a sequence of imperative actions.
global-do ::= do identifier [< argument-list > ] ( role-instantiation-list ) ; role-instantiation-list ::= role-name as role-name ( , role-name as role-name )*
A do starts with the keyword do followed by the name of the target protocol, a an optional argument list and a role instantiation list, and is terminated by a semicolon.
The protocol identifier should correspond to a known protocol. The parameter list and role list in the definition of the target protocol must respectively be of the same length as the argument list and role instantiation list present in the do construct. For each R1 as R2 element where specified, where R1 and R2 are role-names, in the role instantiation list, R1 must be a role of the current protocol and R2 a role of the target protocol.
A local protocol declaration has the following syntax.
local-protocol-decl ::= local protocol identifier at role-name local-protocol-definition local-protocol-definition ::= [ < parameter-list > ] ( role-list ) local-interaction-block
A local protocol declaration starts with the keywords local protocol. It is followed by a name for the protocol, the name of the local role, a list of roles and a local interaction block. The role list is a comma-separated list of identifiers each preceded by the keyword role.
The body of a local protocol declaration is a local interaction block. A local interaction block is a local interaction sequence enclosed by curly braces { }.
A local interaction sequence is a possibly empty sequence of local interactions: send and receive message transfer, choice, parallel, recursion and continue. interruptible
A local message transfer is either a send or a receive of a message to or from a role.
local-send ::= ( message-signature | identifier ) to role-name ; local-receive ::= ( message-signature | identifier ) from role-name ;
Both send and receive start with a message-signature. The role-name immediately after the from keyword specifies the sender of the message that has to be sent. The role-name after the to keyword specifies the receiver of a message that is expected to be received.
The choice construct specifies that one role chooses one out of a set of interaction blocks for the protocol to follow. The choice of interaction block is mutually exclusive; the conversation follows exactly one interaction block.
local-choice ::= choice at role-name local-interaction-block ( or local-interaction-block )*
A choice starts with the keywords choice at, followed by a role-name designating the role responsible for the choice. This is followed by a list of global interaction blocks separated by the keyword or. The interaction block list cannot be empty.
The parallel construct specifies a set of interactions that can happen concurrently.
local-parallel ::= par local-interaction-block ( and local-interaction-block )*
A parallel starts with the keyword par, followed by a list of global interaction blocks separated by the keyword and. The interaction block list cannot be empty.
The recursion construct is used to specify loops in the control flow of a protocol.
local-recursion ::= rec identifier local-interaction-block local-continue ::= continue identifier ;
A recursion point is specified by the keyword rec and an identifier label for this point. Within the following global interaction block, the keyword continue followed by a recursion point identifier specifes that the control flow of the protocol should return to that point.
The interruptible construct is used to specify the interrupts that can be thrown or caught within an interaction block.
local-interruptible ::= interruptible local-interaction-block with { ( throw | catch | throw catch ) } throw ::= throws message-signature ( , message-signature )* ; catch ::= catches message-signature from role-name ( , message-signature from role-name)* ;
An interruptible starts with a keyword interruptible followed by a local interaction block specifying the main behaviour. This is followed by either a list of the keyword throw or the keyword catch, each followed by a message signature.
The do construct specifies that the interactions specified by another protocol (called the target protocol) should be performed inline with the current conversation.
local-do ::= do identifier [< argument-list > ] ( role-instantiation-list ) ; role-instantiation-list ::= role-name as role-name ( , role-name as role-name )*
A do starts with the keyword do followed by the name of the target local protocol, a an optional argument list and a role instantiation list, and is terminated by a semicolon.
This chapter describes the conditions for Scribble protocols to be well-formed, i.e. giving meaningful protocols, beyond the basic syntax defined by the language grammar. This is necessary because some of the protocols are unsafe or inconsistent even if they follow the grammar (for example, two parallel interactions from the same sender to the same receiver with the same message signature violates linearity and leads to a confusion at the receiver). Therefore, understanding well-formendess is also useful for writing safe protocols. In the following we outline key conditions for well-formedness, which will be enough for most protocols.
All of these conditions are checked algorithmically in an efficient manner by Scribble supporting tools.
A well-formed Scribble global protocol observes the following conditions.
In a global-choice, of the form choice at A block1 or … or blockn, the following conditions should be satisfied.
In a global-parallel, of the form par block1 and … and blockn, the following conditions should be satisfied.
This document was translated from LATEX by HEVEA.