```javascript
{__ThisMode__ = VNone; __StringData__ = VNone; __Strict__ = VNone;
__SourceText__ = VNone; __SetPrototypeOf__ = <fun>;
__ScriptOrModule__ = MNNull; __Realm__ = VNone;
__ProxyTarget__ = VNone; __ProxyHandler__ = VNone;
__InitialName__ = VNone; __GetPrototypeOf__ = <fun>; __Prototype__ =
MNNotNull(ObjectLocationIntrinsic IntrinsicObjectPrototype);
__PreventExtensions__ = <fun>; __ParameterMap__ = VNone;
__OwnPropertyKeys__ = <fun>; __Name__ = VNone;
__IsExtensible__ = <fun>; __IsClassConstructor__ = VNone;
__HomeObject__ = VNone; __HasProperty__ = <fun>;
__GetOwnProperty__ = <fun>; __GeneratorState__ = VNone;
__GeneratorContext__ = VNone; __GeneratorBrand__ = VNone;
__FormalParameters__ = VNone; __Extensible__ = VSome T;
__Environment__ = VNone; __Env__ = VNone; __ECMAScriptCode__ = VNone;
__Delete__ = <fun>; __DefineOwnProperty__ = <fun>;
__ConstructorKind__ = VNone; __Construct__ = VNone; __Call__ = VNone;
__BoundThis__ = VNone; __BoundTargetFunction__ = VNone;
__BoundArguments__ = VNone; __AsyncGeneratorState__ = VNone;
__Properties__ =
List.(:)
({_PropertyKey__ = Str "n";
  _Descriptor__ =
    {__Writable__ = VSome T;
      __Value__ = VSome (Numeric (Number (Float 42.)));
      __Set__ = VNone; __Get__ = VNone; __Enumerable__ = VSome T;
      __Configurable__ = VSome T}},
[]);
__ObjectType__ = OrdinaryObject; _O_Set__ = <fun>; _O_Get__ = <fun>;
__ConstructorSteps__ = VNone; _AdditionalSlots__ = List.[]}
```

<caption>Figure 4.2: Internal representation of the object `{n: 42}`.</caption>

1. If `foo` is true

• Let `bar` be false

2. If `bar` is ...

<caption>Figure 4.3: Example of algorithmic steps in which a local environment is necessary.</caption>
```javascript
type completionType=
| Normal
| Break
| Continue
| Return
| Throw
```

```javascript
type completionValue<a>=
| Ok a
| Abruption maybeEmpty<value>

type completionTarget:=
  maybeEmpty<string>
```

```javascript
type completionRecord<a> = (_Type_ : completionType,
                                _Value_ : completionValue<a>,
                                _Target_ : maybeEmpty<square>)
```

<caption>Figure 4.4: Skel Formalization of ES Completion Records</caption>

### 4.1.3 Completion Record and the ECMAScript Error Handling
(?! monad)

Most ES operations do not directly return values, they return *completion records*<fnref n="4" /> instead. A Completion Record describes the runtime propagation of values and control flow. This record is composed of three fields: a kind (either a result, a break out of a loop, a return of a function, or an exception being thrown), an optional value, and in the case of a break or continue, a target.

In theory, a completion record should only hold ES language values (Null, Undefined, Boolean, Number,BigInt, String, Symbol, and Object) or be empty. In practice, it is used to return many other constructions.<fnref n="5" /> If we consider the ` value(\_V)` abstract operation, the completion record given as input can hold either a Value or a Reference in its `_Value_` field. Many such examples litter the specification. Hence, we consider completion records to be polymorphic in what their “value” field holds. We declare such completion records as `type completionRecord<a>`. Figure 4.4 defines the types corresponding to the contents of this record: the `completionType` holds the kind of the record, and the `completionValue` is either an `Ok` polymorphic constructor that contains the value of a non-abrupt computation or an abruption. An ES abrupt Completion Record is one whose type is not **normal**. For instance, a **throw** record has an exception

<footnote n="4">4. https://tc39.es/ecma262/2021/#sec-completion-record-specification-type</footnote>

<footnote n="5">5. In early 2022, the specification changed to accept any value and not just language values, see https://github.com/tc39/ecma262/pull/2547</footnote>
```javascript
type out<a> =
| Success completionRecord<a>
| Anomaly anomaly
```

```javascript
type anomaly =
| AbruptAnomaly completionRecord<()>
| StringAnomaly string
| NotImplemented
```

<caption>Figure 4.5: Out and Anomaly Declarations</caption>

object as completion value, a **return** record has an optional value, and a **break** record has empty. Due to the aforementioned specification issues where non-values may be returned, we store the optional value in a separate constructor to be able to return it independently of the completion type. Finally, the `completionTarget` holds the optional string representing the target, typically used for a `break` to a label. An ES completion record for values has type `completionRecord<maybeEmpty<value>>`.

We next define a type `out` (Figure 4.5) composed of two constructors, `Success` for *successful computations* and `Anomaly` for anomalies, which intuitively corresponds to a failure of the specification, e.g., when an assertion does not hold. A successful computation is one that returns an ES completion record, either `Normal` or `Abrupt`. The `Anomaly` constructor captures incorrect computations. In the specification, anomalies can be raised by assertion failures or when it is explicitly written that an abstract operation call must not return an `Abruption`. The specification authors informally guarantee that these failures never occur.

The `Anomaly` constructor is of type `anomaly`. It has three type constructors: `AbruptAnomaly` holding a completion record in case an evaluation returns an unexpected abruption, `StringAnomaly` that contains textual information about an anomaly—when an assertion of the specification is broken or when an implementation-dependent operation fails, and the `NotImplemented` signaling that we have not yet implemented some feature.

ES abruptions are propagated through an abstract method called `ReturnIfAbrupt`. Basically, this method gets a completion record and either returns the value of the `_Value_` field in case of a normal completion, or it propagates the abruption.

In cases of an abstract operation or a recursive evaluation, the specification uses the prefix `?` to indicate that `ReturnIfAbrupt` has to be applied to the resulting completion. This operator is a monadic bind for a variant of the classic exception monad. The other operator used in the specification is `!:` it behaves similarly to `?` on a normal result, but it asserts an abruption cannot occur. We thus model it as transforming an abrup-
<figure><img src="image_22.png" /><figcaption>Figure 4.6: The Model of ? and !.</figcaption></figure>

tion into an anomaly. These behaviors are reflected in the flow-chart presented in Fig-
ure 4.6, presenting respectively out_q<sub>(α,β)</sub> (red arrows) for the ?, and out_b<sub>(α,β)</sub> (orange
arrows) for the !.

We define them as the monadic binders of the combination of st and out. We put
the state monad outside as we want to return a state in the case of an exception.

val out_q<a,b>: st<out<a>> → (a→st<out<b>>>) → st<out<b>>
val out_b<a,b>: st<out<a>> → (a→st<out<b>>>) → st<out<b>>
val outencoer<out<ab>, b> : out<ab> → (a → st<out<b>>>) → st<out<b>>
binder ?out = out_q
binder !out = out_b

We also define getters (getNormal, getAbrupt, ...) to extract values from a
completionRecord, and return functions (retAnomaly, retAbrupt, retNormal, ...) for
successful and anomaly computations. Note the use of the abruptionCoerce operation
that is only defined for completion records that are abruptions. It is the identity, but it
changes the type parameter of the completion record. What follows shows how faithful
is the translation of these types of algorithmic steps in Skel. The annotation τbar is the
type of bar.
```javascript
type cf<a> =
| ReturnControl a
| ContinueControl

val cf_ret<a> (v:a) -> cf<a> =
  ReturnControl<a> v

val cf_cont<a> : cf<a> =
  ContinueControl<a>
```

```javascript
val cf_bind<a> : cf<a> ->
  ((() -> cf<a>) ->
   cf<a>)
binder @cf := cf_bind

val cf_res<a> : cf<a> -> (a -> a) ->
  a
binder <cf := cf_res
```

<caption>Figure 4.7: The controlFlow type with binders and setters</caption>

1. let `bar` be ? `AbstractOperation(foo)`

2. Return `bar`

```javascript
let bar =?out abstractOperation(foo) in
retNormal<τbar> bar
```

### 4.1.4 A Control-Flow monad

As said earlier, the ES specification uses imperative control flow, such as returning in the middle of an algorithm. In Figure 4.7, we introduce the `type cf<a>`. It represents computations that can either continue or that terminate with a result of type `a`. It comprises two constructors: `ReturnControl`, to return a result of type `a`, and `ContinueControl` to continue the execution.

We define a monadic binder `cf_bind`, a function `cf_res` to extract the value from a `cf<a>` term, a function `cf_ret` to break the control-flow and return a value, and a function `cf_cont` to signal the execution should continue.

We illustrate in Figure 4.8 the translation of algorithmic steps in Skel, with and without the control-flow monad. We recall that we use the forms `let True = ... in ...` to test whether a value is true, and `let False = ... in ...` to test whether it is false. We also write `foo;@ bar` for `let _ =@ foo in bar`. Despite the slight overhead in notation, the control-flow approach is closer to the algorithmic steps and can be consistently applied to deal with the typical case of a conditional that returns without an else branch. One can achieve a similar behavior without the control flow monad at the
1. If `foo` is true Return 1

2. If `bar` is true Return 2

3. If `baz` is true Return 3

4. Return 4

```pascal
(*no control-flow monad*)
branch let True = foo in 1
or
    let False = foo in
        branch let True = bar in 2
        or
            let False = bar in
                branch let True = baz in 3
                or
                    let False = baz in 4
            end
        end
end
```

```pascal
(*control-flow monad*)
let result = <cf
    branch let True = foo in cf_ret<int> 1
    or      let False = foo in cf_cont<int>
        end; @cf
    branch let True = bar in cf_ret<int> 2
    or      let False = bar in cf_cont<int>
        end; @cf
    branch let True = baz in cf_ret<int> 3
    or      let False = baz in cf_cont<int>
        end; @cf
    cf_ret<int> 4
in result
```

<caption>Figure 4.8: Code with and without Control Flow Monad.</caption>

cost of nested branching. It is possible to avoid the nesting of branching by hoisting all the branches at top-level. This results in the following code.
```javascript
branch let True = foo in 1
or      let False = foo in let True = bar in 2
or      let False = foo in let False = bar in let True = baz in 3
or      let False = foo in let False = bar in let False = baz in 4
end
```

The reason previous conditions are repeated is because there is no guarantee that the evaluation of a branching will consider branches in declaration order. In addition, using a collecting semantics (where all branches are considered) would give the wrong result if we did not restate all conditions.

We define `st<cf<out<a>>>` type as the combination of the three monadic types, and accordingly, the definitions of the binders and return functions as `bind (@)`, `cf_out (<)`, `cont`, and `ret`. Our general approach is to encapsulate all the algorithmic steps in this type, returning an `st<out<a>>` at the end of every function that may raise an exception. To this end, we start each algorithm with `let result =<` to enter the full monad with control, and we exit the control monad at the end of the algorithm with `in result`. Figure 4.9 gives a variant of Figure 4.8 with exceptions. Notice that the only thing that changes is the first step and the use of the appropriate monadic binders for the type `st<cf<out<a>>>`.

Despite the closeness to the algorithmic steps, the latter figure, in lines 3, 5, and 7, shows redundancy of code in the `or` branches. Indeed, each time the condition is not satisfied, we have to explicitly state that the evaluation continues. To avoid doing so, we define two boolean binder-like functions, `ifTrue` and `ifFalse`, for introducing partiality in branchings. The `ifTrue` binder, denoted as `@t`, evaluates the rest of the branch when given the `True` value and directly returns a `ContinueControl` when given the `False` value. The following code applies the `ifTrue` binder to the example in Figure 4.9.

```javascript
let result =<
    branch foo;@t throw<int> fooError end;@
    branch bar;@t ret<int> 2 end;@
    branch baz;@t ret<int> 3 end;@
    ret<int> 4
in result
```
1. If `foo` is true throw `FooError`

2. If `bar` is true return 2

3. If `baz` is true return 3

4. Return 4

1. let result = <

2. branch let True = foo in throw <int> fooError

3. or let False = foo in cont <int> () end; @

4. branch let True = bar in ret <int> 2

5. or let False = bar in cont <int> () end; @

6. branch let True = baz in ret <int> 3

7. or let False = baz in cont <int> () end; @

8. ret <int> 4

9. in result

<caption>Figure 4.9: Variant of the Figure 4.8 with Exceptions.</caption>

### 4.1.5 A Real Example in Skel

In this section, we show the effectiveness of the design choices introduced in the previous sections. We proceed by presenting the formalization of the `GetValue` abstract method as an example. This method, presented at the top of Figure 4.10, is one of the most used methods in the specification, as it is often called after the evaluation of syntactic constructors of the language. It takes `V` as input, a completion record containing either a value or a reference, and returns a value as output. In a nutshell, if `V` is a value, `GetValue` returns it, and if it is a reference, `GetValue` acts like a binding resolver to obtain a primitive value from an `Object` or an `Environment Record`.

The reference<fnref n="6" /> type is a record that contains four fields, including the `[Base]` field that holds an environment record or an `ES` value and three other fields not relevant here. Our mechanization in Skel specifies references as records too.

We now describe step-by-step how we formalize this method (the code is collected as a single function at the bottom of Figure 4.10). The type mixing values and references is the specified type `valref` defined as `| Val value | Ref reference`. The argument of `GetValue` thus has type `out <valref>`. We highlight the code that does not

<footnote n="6">6. https://tc39.es/ecma262/2021/#sec-reference-record-specification-type</footnote>
1. `ReturnIfAbrupt(V)`.

2. If `Type(V)` is not `Reference`, return `V`.

3. If `IsUnresolvableReference(V)` is `true`, throw a `ReferenceError` exception.

4. If `IsPropertyReference(V)` is `true`, then

a. Let `base` be `V.[[Base]]`.

b. Let `baseObj` be `! ToObject(base)`.

c. Return `? baseObj.[[Get]](V.[[ReferencedName]], GetThisValue(V))`.

5. Else,

a. Let `base` be `V.[[Base]]`.

b. `Assert: base` is an `Environment Record`.

c. Return `? base.GetBindingValue(V.[[ReferencedName]], V.[[Strict]])`.

1. `(*1*) let v =%returnIfAbrupt v in`
2. `(*2*) branch valref_Type(v, T_Ref);@f let Val v = v in ret<value> v end;@`
3. `(*N*) let Ref v = v in`
4. `(*3*) branch isUnresolvableReference(v);@t`
5. throw<value> referenceError end;@
6. `(*4*) branch let True = isPropertyReference(v) in`
7. `(*a*) let R_val base = v.base in`
8. `(*b*) let baseObj =! toObject(base) in`
9. `(*N*) let baseObj =/o baseObj in`
10. `(*c*) let thisVal =? getThisValue(v) in`
11. `(*c*) let r =? baseObj._Get_(v.__ReferencedName__, thisVal) in`
12. `(*c*) ret<value> r`
13. `(*5*) or let False = isPropertyReference(v) in`
14. `(*a*) let base = v.base in`
15. `(*b*) assert_true<(reference, type_ref)> ref_Type (base, T_R_ER);@`
16. `(*N*) let R_ER base = base in let base =/er base in`
17. `(*c*) let r =? base._GetBindingValue_(v.__ReferencedName__,`
18. v.__Strict__) in`
19. `(*c*) ret<value> r`
20 end

<caption>Figure 4.10: The ECMAScript's `GetValue(V)` and its Skel formalization</caption>

correspond to the ES algorithmic steps, i.e., code that is an overhead of the Skel formalization. It is necessary for typing reasons (extracting a value from a variant type) or
transforming a heap location into its contents.

The first step of the abstract method applies `ReturnIfAbrupt` on `V`. In case it is an abruption, the method propagates the completion record to the caller. Otherwise, it extracts the `completionValue`. To model this, we use the `/\%/returnIfAbrupt` monadic binder. We could directly write `let v =@ returnIfAbrupt<(valref, value)>(v)`, but this requires specifying the polymorphic type components, which is not necessary for binders as they are inferred. We are working on extending the type inference to make polymorphic annotations unnecessary and thus be closer to the specification. If `V` is a normal completion, the newly bound `V` will have type `valref`.

The next ES step inspects the type of `V`. If it is not a reference, hence a value, we return it. Otherwise, the `@f` implicitly continues the execution. Then, in Skel's line 3, we can safely extract `v` from the `Ref` type constructor. Now `v` has type `reference`.

Step 3 follows the same pattern as step 2: An *unresolvable* reference is one that has *Undefined* or *Null* as [[Base]]. In this case, a *ReferenceError* is thrown. In Skel, we proceed straightforwardly. If the reference is *unresolvable*, we throw a *referenceError* of type value. The `throw<a>` function takes an error object constructor as an argument. Then, it returns an abrupt `completionRecord` that contains as a `completionValue` a reference error object.

In case the reference is resolvable, step 4 inspects whether `V` is a *property reference*. A *property reference* is a reference that has a non-null, defined base value of type `value`. Step 4.a. assigns the base value stored into the reference to the variable `V`. In line 6 of the Skel formalization, we access the record field. In the same line, we make an inline pattern matching, expecting the base value to be of type `value` (`R_val`). Now `base` is a primitive value, meaning one of type *Boolean*, *String*, *Symbol*, *BigInt*, or *Number*. Then, line 7 describes Step 4.b. The primitive value in `base` is cast to an object. The method `ToObject`, transforms a primitive value into an object, raising an exception when the value is *Undefined* or *Null*. This operation call is prefixed by `!`, meaning that this method should never raise an exception. Indeed, dealing with primitive objects prevents from getting an exception<fnref n="7" /> as a result of the cast operation. In Skel, the result of `toObject` is an object location. In line 8, we take the object value from the state with the monadic binder `/o`. Finally, Step 4.c. returns the result of the `baseObj`'s [[Get]] object internal method applied to a name representing the referenced value's name and to a value resulting from the call to the `GetThisValue` method.

<footnote n="7">7. In case of an exception, a specification anomaly is then raised.</footnote>
In Skel, we split this step into three. First, the method getThisValue is called on the reference v, assigning its result to the variable thisVal. Note that we make explicit the call to getThisValue, as Skel requires function application to consider fully computed terms as arguments. The call to getThisValue is not pure as the assertion there<fnref n="8" /> is not captured by typing (although we have checked that the reference is indeed a property reference at step 4). We thus use the ? binder, in that case, to extract the pure value or propagate the abruption, if any. Second, once baseObj is set, we call its _Get_ internal method. This method takes v.__ReferencedName__ and thisVal as arguments. The call is prefixed by ?, meaning, again, that if an abrupt result happens, it is propagated to the caller. Finally, we return the result of the call.

If V is not a property reference, then base must be an Environment Record. The Skel else branch, namely Step 5., follows the structure of Step 4. Notice that in 5.b, there is an assertion that we capture in line 14. It can be read as "assert that is true that the reference base-value base is an Environment Record". The ref_Type is a function that takes a tuple of type (reference, type_ref), returning a boolean. The type_ref type constructor T_R_ER represents references with Environment Records as base values. The assert_true is a function that takes as arguments a function f and its arguments a. It propagates an anomaly when the application f a is False or continues to compute in case of a True judgment.

As with most of the algorithms in the Skel mechanization, we need to return a result that is out of the control-flow monad type. The following piece of code thus surrounds the whole algorithm.

let result =< (* GrowValue's algorithmic steps *) in
result

4.1.6 Current Status

We defined a three-steps entry-point to the mechanization. First, we create the environ-
ment in which the code will be evaluated by initializing the interpretation environment<fnref n="9" />.
This operation creates the *Realm*, a record to which all the evaluated ECMAScript
code is associated, the *Intrinsic Objects*, the main *Execution Context*, the *Global Envi-

<footnote n="8">8. https://tc39.es/ecma262/2021/#sec-getthisvalue</footnote>

<footnote n="9">9. https://tc39.es/ecma262/2021/#sec-initializehostdefinedrealm</footnote>
ronment, and the *Global Object*, which can be considered as the standard library of JS.
Second, we parse the script<fnref n="10" />, and finally, we evaluate the script<fnref n="11" />. To execute these
three steps, it is required a significant implementation of the specification, mostly from
[20, Chapters 6 to 10, 18, 19, 20]. Once the runtime environment of the specification is
defined, extending the Skel mechanism comes straightforward.

Concerning the language itself, we defined in Skel a significant subset of ES Syntax
and its evaluation. Unfortunately, no existing parser of JS provides a faithful represen-
tation to ES Syntax. We thus had to choose between implementing our own parser or
translating the AST provided by on-the-shelf parsers. We chose the latter. More pre-
cisely, we use a parser that conforms to the *SpiderMonkey's* Parser API<fnref n="12" />, which is
followed by all parsers we have found. We chose the Flow Parser<fnref n="13" /> library because it
is written in OCaml, which is the language we can instantiate our interpreter into, and
because it is used to manipulate JS in industrial setting. When instantiating the inter-
preter, we define transformations that, given a Flow AST, produces a well-typed ES
AST.

We implemented most of the *Statements*, and *LexicalDeclarations*([20, Chapter 14]). Indeed, these two syntactic production define what a script is([20, Section 16.1]).

For what concerns the *Expressions*([20, Chapter 13]) of the language, we formal-
ized most of the chapter. We are still working on the semantics of some *CallExpres-
sions* and of the function definitions([20, Sections 13.3, 15.5, 15.6, 15.8, 15.9]), as their
evaluation explicitly manipulates continuations of the interpreter code. This prevents us
from start testing interpreter via the ES262 test suite, as function calls are required for
testing. Nevertheless, understanding how the function calls are specified led to the dis-
covery of some places where the manipulation of execution contexts were not properly
described or handled.<fnref n="14" />

Intuitively, an ECMAScript function call first evaluates the actual arguments, bind-
ing them to local variables, before executing the core of the function in this new
environment. The algorithmic steps for processing all the inputs of a function and
then binding them in the function environments are defined in the internal method

<footnote n="10">10. https://tc39.es/ecma262/2021/#sec-parse-script</footnote>

<footnote n="11">11. https://tc39.es/ecma262/2021/#sec-runtime-semantics-scriptevaluation</footnote>

<footnote n="12">12. https://developer.mozilla.org/en-US/docs/Mozilla/Projects/SpiderMonkey/Parser_API</footnote>

<footnote n="13">13. https://github.com/facebook/flow</footnote>

<footnote n="14">14. https://github.com/tc39/ecma262/issues/2400, https://github.com/tc39/ecma262/issues/2409</footnote>
(a) For each element E in list, do

(i) Perform ? Yield(E)

(b) Return **undefined**

<caption>Figure 4.11: yieldable abstract closure</caption>

FunctionDeclarationInstantiation<fnref n="15" />. In step 24 of this method, there is a call to CreateListIteratorRecord<fnref n="16" /> with argumentsList as a parameter, a list of the arguments of the function. An abstract closure **closure**, shown in Figure 4.11, is then defined. It corresponds to a delimited computation that yields the next argument each time it is resumed (the ? in the code is a monadic binders that intuitively propagates an exception if one happens). The specification then creates an **iterator** through the call of the method CreateIteratorFromClosure<fnref n="17" />. Parameters of the call are **closure**, that is a piece of code that will be associated to the **iterator** **iterator**, and `%IteratorPrototype%`, prototype of the object that the method creates. The object is extended with some extra internal slots (step 3-OrdinaryObjectCreate<fnref n="18" />) [[GeneratorState]], [[GeneratorContext]], and [[GeneratorBrand]]. A new execution context is then created, similar to using Run in Section 3.5, and `GeneratorStart`<fnref n="19" /> is called in this context. In the particular case of function calls, this method sets a call to **closure** as a resumption handler. The **iterator** is then suspended, and `CreateIteratorFromClosure` returns it. Then, `CreateListIteratorRecord` binds it to **iterator** and it returns an **iterator** record with **iterator** as the **iterator** object and `%GeneratorFunction`.prototype.prototype.next% as next method of the (suspended) **iterator**. Back to FunctionDeclarationInstantiation, the next step is the call to *IteratorBindingInitialization*<fnref n="20" />. This uses the **iterator** to repeatedly call its *next* method, which itself calls `GeneratorResume`<fnref n="21" />. This makes a context switch that puts the **generator** context as the running execution context, and it resumes it by calling the closure stored in the context code evaluation state. This is similar to

<footnote n="15">15. https://tc39.es/ecma262/#sec-functiondeclarationinstantiation</footnote>

<footnote n="16">16. https://tc39.es/ecma262/#sec-createlistiteratorRecord</footnote>

<footnote n="17">17. https://tc39.es/ecma262/#sec-createiteratorfromclosure</footnote>

<footnote n="18">18. https://tc39.es/ecma262/#sec-ordinaryobjectcreate</footnote>

<footnote n="19">19. https://tc39.es/ecma262/#sec-generatorstart</footnote>

<footnote n="20">20. https://tc39.es/ecma262/#sec-runing-semantics-iteratorbindinginitialization</footnote>

<footnote n="21">21. https://tc39.es/ecma262/#sec-generatorresume</footnote>
```typescript
module IntMap = Map.Make (Int)

module rec T : sig
  type bigInt = Big_int.t
  and float = Float.t
  and int = Int.t
  and 'a intMap = 'a IntMap.t
  and 'a list = 'a List.t
  and string = String.t
end = T
```

<caption>Figure 4.12: TYPES module instantiation</caption>

calling resume in Section 3.5. Running the closure results in the call to the Yield in it, providing the next argument.

Understanding how the function calls are specified led to the discovery of some places where the manipulation of execution contexts were not properly described or handled<sup>22,23</sup>. This resulted into some clarifications and bug fixes, such as the creation of a new execution context for the generator.<sup>24</sup> Links to the specification above are to the current version where the clarifications are included. To read the 2021 version, replace https://tc39.es/ecma262/ with https://tc39.es/ecma262/2021/.

## 4.2 Interpreter Evaluation

### 4.2.1 Interpreter Instantiation

To instantiate an interpreter generated by `necroml`, we need to provide an implementation to the unspecified types and terms.

Regarding the unspecified types, although the ES specification in Skel consists of 15k LOC, only 6 types need a definition. We show the instantiation of the TYPES module in Figure 4.12. Notice that we could have left unspecified four data types out of six, by writing a library defining the `list` and `intMap` in Skel.

<footnote n="22">22. https://es.discourse.group/t/execution-context-suspension-and-resumption/756</footnote>

<footnote n="23">23. https://github.com/tc39/ecma262/issues/2400</footnote>

<footnote n="24">24. https://github.com/tc39/ecma262/pull/2398</footnote>
Concerning terms, we have 450 of these unspecified elements in our skeletal semantics. We instantiate some of the unspecified functions—the ones that the interpreter uses-, leaving the others returning *NotImplemented*. Finally, we define a parsing method to transform a JavaScript program into an ECMAScript AST. To this end, we rely on the Flow Parser AST and convert the result to the (much more complex) AST used by ECMAScript. We are then ready to run examples.

As we said in Section 4.1.6, we have gradually implemented core functionalities of the ES to crash test our specification language Skel and see if it is expressive enough to represent such complex semantics faithfully.

## 4.2.2 Evaluation

We propose two ways of evaluating this work. The first one is to compare our work with previous ones (Framework Comparison), and the second is to describe what JS programs we can execute (Program Execution).

### 4.2.2.1 Framework Comparison

One of the goals of this work is to show visual closeness and maintainability of the proposed formalization. We compare our work with $K_{JS}$ [56] and JSCert [6] by considering the formalization of the *GetValue* internal algorithm. Note that both these formalizations are based on ECMAScript 5.1, an older version of the standard. The ECMAScript standard tripled in size since then and its algorithms are much more complex, including explicit continuation manipulation.

$K_{JS}$ is a set of rewriting rules representing the ES semantics. This means that given an internal method, there are a subset of whole rewriting rules set, matching the method's behaviour. To simplify, we can say that the left hand side component of the rule is rewritten into the right hand side when the conditions allow it. The correctness of $K_{JS}$ is attested by a great coverage of the ES262 test suite. Consider the *GetValue* algorithmic steps in ECMAScript 5.1²⁵. One can notice the differences between the method of the 2021 standard and the one of version 5.1. The old rule can be split in four cases defined by the types that the *GetValue's* parameter V can take. Indeed, V can be either a *reference*, an *object*, the *undefined* value, or a *primitive* value. In Figure 4.13, we present the $K_{JS}$ implementation. The 4 rules concisely cover all the cases.

<footnote n="25">25. https://262.ecma-international.org/5.1/#sec-8.7.1</footnote>
rule GetValue(@Ref(E:Eid,N:Var, Strict:Bool)) =>
    GetBindingValue(E,N,Strict)
rule GetValue(@Ref(O:Oid,P:Var, _)) => Get(O,P)
rule GetValue(@Ref(Undefined, P:Var, _)) =>
    @Throw(@ReferenceError("GetValue",P))
rule GetValue(@Ref(B:Primitive,P:Var, _)) =>
    GetPrimitive(B,P)

<caption>Figure 4.13: GetValue 5.1 written in the K framework.</caption>

In case of `V` being a reference, the `GetValue` is rewritten in a `GetBindingValue`. If it is an object, the definition is rewritten to an object `Get`. In the latter two cases, instead of using the method `IsUnreasolvableReference` and `HasPrimitiveBase`, the authors define two rules, one in which `V` is `Undefined`, which corresponds to an unresolvable reference, and the other by matching the input parameter with a Primitive label, representing a subtype of the ES value type.

We argue our Skel formalization is better for the following reasons. First, we are very close to the textual description of the standard. In fact, when translating it to Skel, we do not need to fully understand its behavior. This suggests that an automated translation, as done in [59], could be achieved. Second, the formalization has not been updated since 2015. Third, the formalization in itself is not easily manipulated by external tools. In contrast, our Skel definition can be used to generate a Coq description, which is not possible with `K`.

We show a part of the formalization of `GetValue` in JSCert in Figure 4.14.<fnref n="26" /> The formalization is a Coq shallow embedding of ES, in pretty-big-step semantics style [15]. As said before, the two main issues with JSCert are maintainability and usability. Regarding the latter, the semantics is too big to be used in the context of Coq induction and inversion (Coq runs out of memory). Using a deep embedding (where the recursive evaluation of the language semantics is not captured using Coq's induction) would help avoid the issue, but doing so requires rewriting the semantics. As Coq descriptions are not easily manipulated by outside tools, this motivated us to redo the semantics in a framework where this issue could be circumvented, hence the current work.

To conclude, neither `Kjs` nor JSCert are easily maintainable, as their approaches are too much embedded in the tools they are using. By having a simple but powerful

<footnote n="26">26. Full code at https://github.com/jscert/jscert/blob/master/coq/JsPrettyRules.v#L5112</footnote>
(** Get value on a reference (returns value) (8.7.1) *)

| red_spec_ref_get_value_value: **forall** S C v, (* Step 1 *)
  red_spec S C (spec_get_value v) (ret S v)

| red_spec_ref_get_value_ref_a: (* Steps 2 and 3 *)
  **forall** S C r (y:specret value),
    ref_is_unresolvable r ->
    red_spec S C (spec_error_spec native_error_ref) y ->
    red_spec S C (spec_get_value r) y

| red_spec_ref_get_value_ref_b_has primitive_base:
  (* Steps 2 and 4 *)
  **forall** v S C r o1 (y:specret value),
    ref_is_property r ->
    ref_base r = ref_base_type_value v ->
    ref_has primitive_base r ->
    red_expr S C (specPrim_value_get v (ref_name r)) o1 ->
    red_spec S C (spec_get_value_ref_b_1 o1) y ->
    red_spec S C (spec_get_value r) y

<caption>Figure 4.14: GetValue 5.1 in JSCert</caption>

specification language, we are able to systematically write code that is very close to the standard and easy to maintain. We migrated from ECMAScript 2020 to ECMAScript 2021 in less that a week of work, by only changing the algorithmic steps that have been modified.

### 4.2.2.2 Program Execution

After instantiating the interpreter, we started to test it gradually. We show, in Figure 4.15, an example of such a test program: a non-trivial manipulation of an object, by defining an object and modifying its properties via property accessors. In the first line of the program, we define an array by assigning to the variable `a` an array literal with elisions. The right part evaluate as an array object value that does not have a mapping to values in positions 0, 2, 3, and 5. The indices 1, 4, and 6 are respectively mapped to the string `"one"`, the string `"two"`, and to the number 3. Then, in the second line, we create a new ordinary object and assign it to the variable `o`. We define two properties in
It has a major drawback, however. If the design choices are not correct, one cannot
manipulate the mechanization to modify it, and one must instead redo it using different
choices. JSCert is a pretty-big-step [15] Coq definition of ECMAScript 5.1. It consists
of an inductive definition, a recursive definition, and a correctness proof showing they
match. The goal of the inductive definition is to prove properties of the language and of
JS programs, whereas the recursive definition can provide an OCaml interpreter using
Coq's extraction mechanisms. The mechanization is fairly close to the specification
for people who can read Coq code, and the test suite can be run using the extracted
interpreter. JSCert has two flaws, unfortunately. It is difficult to maintain, as one has to
update two formalizations and a proof. In addition, and most importantly, JSCert uses
Coq's induction to represent the recursive evaluation of the language. This shallow
embedding results in a definition of a semantics as an inductive definition consisting
of about 1000 rules, which is too large to prove properties of the language. Some
authors of JSCert built upon this work to derive systematic and reusable definition of
semantics [9, 8].

An other approach to the formalization of JavaScript is to translate it to a much sim-
pler language, whose semantics is less complex. This is done for instance in the setting
of [25], where JavaScript programs are translated to a simple language called λ<sub>JS</sub>. This
work is based on ECMAScript versions 3 and 5. The authors empirically show that the
translation of JS programs is correct by running the JS test suite. As this formalization
is not textually close to the specification, it is difficult to assess whether it actually cap-
tures the language beyond running the tests. In addition, the translation has not been
updated since 2015, in particular it does not include the many changes to the core
data structures and algorithms from ECMAScript 6 (or ECMAScript 2015). Attempts to
formalize λ<sub>JS</sub> in Coq<sup>27</sup> uncovered several issues with the desugaring process that were
not witnessed by testing. It did not lead to a formal mechanization of the language.

Alternatively, one may use an existing framework designed to describe and ma-
nipulate semantics. K<sub>JS</sub> [56] is a complete mechanization of ECMAScript 5.1 in the K
framework. It provides an executable interpreter of JS directly from the semantics with
no additional effort. This framework is not suitable to analyse the language itself as
it only provides tools to reason about the execution of programs. In addition, there is
no evidence that the mechanization can be easily maintained: although JS has sig-
nificantly evolved since ES 5.1 (the specification has more than doubled in size), the

<footnote n="27">27. https://github.com/tilk/LambdaCert</footnote>
mechanization has not been updated. Indeed, works such as JSExplain [16], a JS interpreter written in OCaml, show that updating an ES formalization is far from being a trivial issue. The power of the K framework comes at the cost of additional complexity in the description of languages in it, which hinders maintainability and closeness to the specification.
<figure><img src="image_23.png" /></figure>
PART III

Distributed Semantics
<figure><img src="image_24.png" /></figure>
# AN EXECUTABLE SEMANTICS FOR DISTRIBUTED IoT APPLICATIONS

## Contents

<table><tr><td>5.1 Context</td><td>121</td></tr><tr><td>5.2 WEBI: A Formal Semantics to IoT Applications</td><td>123</td></tr><tr><td>5.2.1 The WEBI Configuration</td><td>123</td></tr><tr><td>5.2.2 Semantics</td><td>127</td></tr><tr><td>5.2.3 Example: The Cost of Non-Determinism</td><td>145</td></tr><tr><td>5.3 A Scheduler for WEBI</td><td>155</td></tr><tr><td>5.3.1 Semantics</td><td>155</td></tr><tr><td>5.3.2 Equivalence of the Scheduler and the WEBI Semantics</td><td>168</td></tr><tr><td>5.3.3 Executing the Example of Section 5.2.3 in Skel</td><td>177</td></tr></table>

« Mi muovo! So parlare! Cammino! »

- Pinocchio, C. Collodi

## Introduction

In Chapter 4, we applied the approach presented in Chapter 3 to describe a Skeletal Semantics of JavaScript's specification, handling the effects of the language by carefully choosing monads and combining them, hiding most of the information in the meta-environment of Skel. Nevertheless, despite JavaScript's intrinsic complexity, the model is mainly deterministic. Indeed, except for the `for-in` construct, which loops on a set of ECMAScript's values, the rest of the language constructs behave sequentially.
Essentially, until now, we dealt with formalizing programming languages, reasonably complex to represent but *deterministic*.

In this chapter, we investigate Skel from another perspective. We want to explore and study a non-deterministic model with more behavioral complexity than the languages we described before. In particular, we write a Skeletal Semantics of a model representing the behavior of distributed systems. The model represents interactions among the server tier, the client tier, and smart devices, describing the Internet of Things (IoT). Indeed, connected devices interact with the physical world, possibly changing its state. The goal is to derive an interpreter from this model's Skeletal Semantics and study its usability.

To this end, we present first a small-step semantics of a distributed model we call WEBI. We also set design choices for writing an interpreter-oriented version of WEBI in Skel. This model is complex in its evolution, producing possibly infinite execution traces. Hence, the interpreter we generate using `necroml` does not scale, possibly never producing an output on non-trivial programs. Thus, to execute and study it, we tame its non-deterministic behavior. We define constraints and a scheduling policy for making it executable. The scheduling policy we describe exploits interleaving invariants between the tiers' code execution. These invariants permit factorizing different equivalent traces by permuting trace elements when possible. We say that two different traces are equivalent if they manipulate the world's state in the same way—a world manipulation results from an interaction between devices and the real world. For example, turning on a connected heater in the living room changes the temperature read by a thermometer, making this new digital value representative of the world state. Then, the order of these actions matters. Opening a window before or after activating the heater changes the state of the world. We define these invariants to preserve the ordering between sensitive world manipulations resulting from the tiers' code execution.

This chapter has a double interest:

1. Show that Skeletal Semantics and Skel easily capture non-deterministic models,

2. Pave the way to further formal analyses on distributed IoT applications.

We structure the chapter in the following way. Section 5.1 provides context and discusses the previous work. Section 5.2.1 introduces the model by discussing its components, and Section 5.2.2 introduces both WEBI's small-step and Skel semantics. Moreover, we present a design for the evaluation function that exploits Skel features for writ-
ing non-deterministic semantics. Afterward, we show how to derive a non-deterministic concrete interpretation, using a particular interpretation monad and a way to obtain collecting semantics. Section 5.2.3 shows a simple example of an application that does not scale on this model, forcing us to tame the non-deterministic behavior. The motivation comes with the writing of the evaluation function, which is ineffective with the collecting behavior, essential for moving towards applying analysis techniques. Hence, Section 5.3.1 proposes a scheduler for WEBI, which bounds the evaluation function's non-determinism. We conclude with Sections 5.3.2 and 5.3.3, respectively presenting an equivalence theorem for the scheduled semantics alongside the sketch of its proof.

## Contribution

* a Skel formalization of WEBI.

* a scheduler for constraining the non-determinism of the model.

* a proof sketch of equivalence of the scheduler semantics.

* an OCaml interpreter of the model.

# 5.1 Context

Several questions related to security and safety spawned as soon as the interest of private companies grew toward IoT devices and applications. Many IoT products are available on the market, making such distributed systems part of our daily life. Every device connected to the internet can be attacked, making academic studies on IoT relevant. In this context, formal methods and the security scientific community are interested in finding ways to detect and prevent security flaws. To summarize, we can factorize the scientific question into the following: *How can an attacker exploit these systems to gain information or control?*

Many works define desugaring of the semantics of existing languages for analyzing IoT applications. For example, SaiNT [13], Soteria [14], and ProvThings [74], among many others, perform static analysis techniques on these distributed programs that rely on real-world languages, such as Groovy [2]. These works aim to detect information
about security flaws concerning this software category. Their analysis techniques are
standard, comprehending mostly taint analysis and some abstract interpretation and
symbolic execution. Nevertheless, the focus of these works is more directed toward
security. Indeed the languages they formalize fit the security purpose, not aiming to be
either a correct or a complete implementation of the semantics.
Moreover, if one wants to use the same techniques of analysis in other languages
means redefining the tools without guarantees that the approach can scale. Indeed,
modeling distributed systems is a problem far from being trivial. The complexity of dis-
tributed systems comes when each actor/tier (server, client, database) uses a different
language, and programs run on different execution contexts. The cost of analyzing
these programs individually and putting together intermediate results is computation-
ally expansive. Additionally, some attacks are not detectable on these models, such
as the cyberphysical ones. These non-digital and indirect attacks trigger a cascade of
events in the physical world that leads to some malfunction.

Formal models to capture the semantics of distributed systems exists, and they are
concerned more with client/server models. For example, the semantics of hop.js [11]
elegantly describes the semantics of the language. Still, this is a semantic definition
of a language with no other purpose than mathematically explaining the programming
language's behavior and its programs. Indeed, not defining other tiers, such as the
device one, makes it impossible to use the model to represent some non-deterministic
interleavings that may provoke cyberphysical attacks.

This chapter proposes a novel semantics called WEBI, implemented in Skel. This
model is an extension of the essence of [11], and it is designed to capture the be-
havior of IoT programs executing in a unique execution context. This choice alleviates
some issues related to the analysis of distributed systems. What we describe in the
manuscript relates more to semantics than analysis, discussing issues and limits. Nev-
ertheless, we show that we can exploit Skel to define collecting semantics, paving the
way for future studies toward program analysis. The model is parametric on the tier
languages; we instantiate it with toy languages. However, this does not limit its use, as
the model can be instantiated with some JavaScript extensions [34, 33], describing the
semantics of multi-tier languages such as hop.js.
## 5.2 WEBI: A Formal Semantics to IoT Applications

This section presents a small-step semantics of WEBI, designed for capturing interactions between different tiers in the context of IoT applications. The actors we consider are:

* Web services that provide services to the clients.

* Web clients that request services.

* Smart objects, which are objects connected to the web. We consider devices with sensors—electronic components that transform physical data into digital data—and actuators—electronic components that transform digital data into physical data.

### 5.2.1 The WEBI Configuration

A WEBI configuration is a 7-uple containing all the information about the actors in the model, namely clients, services, and devices. We write the configuration as conf, and its extensively represented as:

$$ \{WebServices, \mathcal{L}, I, HM, SS, CC, IC\} $$

In the following paragraphs, we explain all the WEBI configuration in detail. In Table 5.1, we summarize the notation.

**WebServices.** The WebServices component is a function

$$ \text{WebServices} : \text{url} \rightarrow (\text{service}, \text{hostname}) $$

mapping *urls*, which we conceive as a generic way to encode the unique address of a web service, to the actual service and hostname. The hostname is an identifier for the server hosting the service. We let the *WebServices* to be implicit in the WEBI configuration, because it is never changed by the WEBI rules.

**World's Events Record** $\mathcal{L}$. The $\mathcal{L}$ component is a record of the *world's events*. With world events, we mean statements or data representing some natural condition of an
<table><caption>Table 5.1: WEBI summary of notation</caption><thead><tr><th>Symbol</th><th>Description</th><th>Skel type</th></tr></thead><tbody><tr><td>wo</td><td>world oracle</td><td>(L, E) → (pe, t)</td></tr><tr><td>E</td><td>set of possible events that can occur in the world</td><td>list&lt;event&gt;</td></tr><tr><td>conf</td><td>a webi configuration &lt;L, I, HM, SS, CC, IC&gt;</td><td>webiConfiguration</td></tr><tr><td>WebServices</td><td>mapping between URLs and related services</td><td>url→((var, sr_stmt), hostName)</td></tr><tr><td>L</td><td>list of located physical events: either actuator-produced events a, d, t or sensed-events pe, d, t</td><td>logEvents</td></tr><tr><td>I</td><td>set of initializers</td><td>initializers</td></tr><tr><td>CC</td><td>set of web clients (cc)</td><td>webClientConfigurations</td></tr><tr><td>SS</td><td>set of web server configurations (ss)</td><td>runningServiceConfigurations</td></tr><tr><td>IC</td><td>set of smart objectconfigurations (ic)</td><td>deviceConfigurations</td></tr><tr><td>HM</td><td>hosts memory: h → μ<sub>h</sub></td><td>hostMemories</td></tr><tr><td>Π</td><td>sequence of WEBI rule applications</td><td>trace</td></tr><tr><td>h</td><td>name of a host</td><td>hostname</td></tr><tr><td>μ<sub>h</sub></td><td>memory of the host of name h</td><td>hostMemory</td></tr><tr><td>u</td><td>url</td><td>url</td></tr><tr><td>v<sub>a</sub></td><td>serialized value</td><td>serializedValue</td></tr><tr><td>v<sub>c</sub></td><td>client value (v<sub>a</sub> ⊆ v<sub>c</sub>)</td><td>cl_val</td></tr><tr><td>v<sub>s</sub></td><td>server value (v<sub>a</sub> ⊆ v<sub>s</sub>)</td><td>sr_val</td></tr><tr><td>P</td><td>program (client or server), note that a value may be a program</td><td>cl_stmt, sr_stmt</td></tr><tr><td>cc</td><td>a running web client configuration in CC (⟨cc, B, T⟩<sup>(j,u)</sup>)</td><td>webClientConfigurations</td></tr><tr><td>ss</td><td>a running service state in SS (ss<sup>(h,j),i</sup>)</td><td>runningServiceConfiguration</td></tr><tr><td>sc</td><td>a running service configuration (ss)</td><td>runningServiceState</td></tr><tr><td>B</td><td>set of call-backs</td><td>cbbacks</td></tr><tr><td>T</td><td>set of chunks</td><td>chunks</td></tr><tr><td>pe</td><td>located physical event</td><td>physicalEvent</td></tr><tr><td>l</td><td>event location</td><td>location</td></tr><tr><td>t</td><td>absolute time</td><td>time</td></tr><tr><td>d</td><td>device ID</td><td>deviceID</td></tr></tbody></table>

object or an environment in the real world, or an action changing its state. Examples could be the statements: “The temperature in the kitchen at 8:00 p.m. is 18°” or “Light turned on at 10:30 p.m. in the bedroom”. We can represent this record as a list of all the actuations and sensor’s detections performed by devices.

On the one hand, an actuation is an action performed by a device through its actuators. This kind of action forcibly changes the state of the world. Indeed, consider the heater example presented in the introduction. The action that turns on the device is an actuation, and the effect (change of the world’s state) is the living room’s temperature increase. We see this as a digital action transformed into a concrete one.

On the other hand, a device that detects physical data from world does not change it; it “queries” it. This operation can be seen as the inverse of an actuation, transforming
concrete data, the world's natural state, into its digital representation.

The *L* record, intuitively, is empty before running the WEBI model. We represent it with the usual empty list notation, [] . Each time a rule needs to record an operation on this list, we write it as op :: *L*, where op is either an actuation or a device sensor result. If op is an actuation, we write it as (a, d, t), where a is the action, d is the device identifier, and t is the time this actuation happened. Otherwise, we write a sensor detection as (pe, t), where pe is the physical event that the device sensed from the world. An example of pe could be: "The living rooms's temperature is 18° Celsius". Concerning the time, we do not provide a specific mapping between real-world time and its digital representation.

Initializers *I*. The *I* element of the configuration is a collection of the initial clients' calls; we call them initializers. We write the model initializer as ((j, u), v<sub>a</sub>), where j is a unique identifier for the client, u is the URL that the booting client j is calling, and v<sub>a</sub> is a value put as a parameter of the initial call. To run the model, we need this set not to be empty in the initial WEBI configuration. Without booting clients, also called initializers, the model will not evolve. We denote the empty *I* as ∅, like the set notation. Indeed, *I* is a set.

Host Memories *HM*. The third element of the WEBI's conf is *HM*, a mapping between host-names *h* and host-memories *µ*<sub>*h*</sub>, which are memories shared among different web services executing on the same host. The letter *µ* refers to the actual data structure acting as memory. The subscript *h* is the name of the host. We write mappings in the usual functional way: *h* ↦→ *µ*<sub>*h*</sub>. We do not specify if the host-memory mappings are total or partial.

Running Services *SS*. The *SS* component is the set of *running services*. We write the element of this set as *ss*, calling it *running web service state*. The running web service state can be either a value or some running program, and we write them respectively as ⟨*sv*⟩ and ⟨*sc*⟩. The first is a *final running service configuration*, a couple (*v*<sub>s</sub>, *µ*<sub>s</sub>), where *v*<sub>s</sub> is a value in the server language and *µ*<sub>s</sub> is the service's memory. The second represents a *running service configuration*. It is a couple (*P*<sub>s</sub>, *µ*<sub>s</sub>), where *P*<sub>s</sub> is a program and *µ*<sub>s</sub> is the local memory of the service. Both the ⟨*v*<sub>s</sub>⟩ and ⟨*sc*⟩ have unique identifiers ((*h*, *j*), *i*), written as a superscript of the running web service state *ss*. This identifier is three-folded:
* *h* is the host-name on which the service is running.

* *j* is a reference to the client who called the service.

* *i* is the identifier of the client's callback that will handle the service return.

### Web Clients CC.
The *CC* component is the set of web clients. We write *CC*'s elements as $\langle\text{boot}\rangle^{(j,u)}$ for the *booting* clients, and $\langle\text{cc}, B, T\rangle^{(j,u)}$ for the *non-booting* ones. We use two combined identifiers as the client's ID: the *j* is the client's unique identifier, and *u* is the URL the client called when booting. The special keyword *boot* in the booting client configuration is a special client's callback waiting for the service's response to initialize the client. Then, the non-booting client is a client that has been already initialized. It is a web client configuration holding three pieces of information: the client program state *cc*, and two sets *B* and *T*. The *cc* can either be a couple composed of a client value *v*<sub>c</sub> and a memory $\mu_c$, or a couple (*P*<sub>c</sub>, $\mu_c$), where *P*<sub>c</sub> is a client program still executing. Then, *B* and *T* are the callback's set—containing all the client's (*j*, *u*) call handlers still waiting for their related service response—and the chunk's set—the callbacks which have already received a result from their related services. Intuitively, we define a *callback* as a program *b* = $\lambda x.P$, where *x* is a free variable waiting to be bound to the result of the related service. Then, given $v_a$, the result of the client call, a chunk *t* of the callback *b* is the substitution of $v_a$ in all *x*'s occurrences in $\lambda x.P$. We write the chunks as $(\lambda x.P, v_a)$. The purpose of not substituting directly the value into the program is to not give the idea of substituting and executing the program *P*. The substitution can also be written as the $\eta$-expansion of the program, resulting in the following: $(\lambda x.\lambda z.P) v_a$. The variable *z* is a free variable in *P* of type unit. To run the program, then one must only apply () to $\lambda z.P[x \to v_a]$. To resume, the variable *x* is bound to the value returned by the service, and *P* is not run.

Each callback and chunk is identified by *i*. We remark that if we pick a callback $b^i$ from the *B* of the client (*j*, *u*), and imagine a function resolving the URLs and returning the host-name (i.e., `solveURL(u) = h`), then we can produce the related service identifier: $((h, j), i)$.

### Device Configurations *IC*.
Finally, the *IC* component is the set of *device configurations*. A device configuration $\langle\mu_d, S, A, \text{perm}\rangle^d$ is defined by $\mu_d$ the device memory, *S* a set sensor, a set of actuators *A*, and a set of permissions *perm*—for interacting
with other tiers, namely the server-tier. Each element of *IC* is signed by *d*, a unique identifier for the device.

## 5.2.2 Semantics

The section presents the formal semantics of the WEBI distributed system model. We present the rules in a small-step style alongside their Skel implementation. Regarding Skel, we present some design choices to make the semantics more precise and suitable for building an interpreter.

Regarding the non-deterministic evaluation function in Skel, we know that the implementation would come pretty straightforward, because we exploit the non-determinism intrinsic in the Skel's *branch* construct. Intuitively, the interpreter will be instantiated with a pseudo-random interpretation monad, which shuffles the branch's list before interpreting its head.

To present the semantics, we structure the following subsections in this way. First of all, we briefly introduce the WEBI transition relation in Section 5.2.2.1. Then, we present the rules and the instantiation of the model. Indeed, in Section 5.2.2.2, we define a set of client-driven rules. The ruleset represents either the client evaluation progression or describes an interaction between the client and server tier. Then, Section 5.2.2.3 proposes rules for handling service-driven rules, and Section 5.2.2.4 describes the device-driven ones, handling interactions between services, devices, and the world's state. We will not discuss the client, the server and the device transition relation, because it would mean to introduce a semantics for each one of the tier's languages. We will only describe some of the main features that the client<fnref n="1" /> and the server<fnref n="2" /> language must have. In the example languages, we wrote variants of the WHILE language presented in Chapter 1.

Finally, Section 5.2.2.5 presents the non-deterministic evaluation function and the OCaml interpreter instantiation.

**Implementation Choices in Skel.** In the Skel implementation we partition the *SS* and the *CC*—written as _SS_ and _CC_ in Skel-WEBI configuration components. We

<footnote n="1">1. https://gitlab.inria.fr/skeletons/webi-in-skel/-/blob/refactor/semantics/webi/clientLanguage.sk</footnote>

<footnote n="2">2. https://gitlab.inria.fr/skeletons/webi-in-skel/-/blob/refactor/semantics/webi/serverLanguage.sk</footnote>
partition the functionally, in order to pick elements from the correct partition efficiently.
The choice we made is to be sure, if any, to make the rules pick the correct web client
and/or web service, avoiding failure.

We define _CC_ as a set of four subsets:

*   `_CC_r` is a subset of `_CC_` (or `CC`) containing all the web clients that can step or
    that are booting. In math-mode, we write it as `CC_r`.

*   `_CC_c` is a subset of `_CC_` (or `CC`) containing all the web clients that call. In math-mode, we write it as `CC_c`.

*   `_CC_t` is a subset of `_CC_` (or `CC`) containing all the web clients that with a non-empty set `B` or `T`. In math-mode, we write it as `CC_t`.

*   `_CC_e` is a subset of `_CC_` (or `CC`) containing all the web clients that have `B` and `T` empty. In math-mode, we write it as `CC_e`. These web clients become inactive in `WEBI`, meaning their `webClientConfiguration` will never change again.

We define the following invariant for the subsets in Definition 1.

**Definition 1** *It holds that $CC_r \cup CC_c \cup CC_t \cup CC_e = CC$, and the intersection between each couple of the subsets of $CC$ is the empty set.*

Moreover, by design, we know that in case of no active web clients in the `WEBI` config-
uration, we can terminate the model's execution. We show this in Definition 2

**Definition 2** *If all the clients are in the subset $CC_e$, no client is active in WEBI. Then, WEBI can terminate.*

Symmetrically, we define subsets of _SS_ as:

*   `_SS_r` is a subset of `_SS_` (or `SS`) containing all the running web services that can step. In math-mode, we write it as $SS_r$.

*   `_SS_a` is a subset of `_SS_` (or `SS`) containing all the running web services that have to issue an actuation request to a device. In math-mode, we write it as $SS_a$.

*   `_SS_g` is a subset of `_SS_` (or `SS`) containing all the running web services that have to issue a reading request to a device. In math-mode, we write it as $SS_g$.
* `_SS_e` is a subset of `_SS_` (or `SS`) containing all the running web services that finished computing. In math-mode, we write it as `SS_e`.

We define the following invariant for the subsets of `_SS_` in Definition 3.

**Definition 3** It holds that $SS_r \cup SS_a \cup SS_g \cup SS_e = CC$, and the intersection between each couple of the subsets of `SS` is the empty set.

Moreover, we argue about services being active. The web services run if a client called them. We present this property in Definition 4.

**Definition 4** If no client is active, then no service is running.

### 5.2.2.1 WEBI Transition Relation

We say that a WEBI's transition relation relates configurations presented in Section 5.2.1; we write it in the following way.

$$ wo, \mathcal{E} \vdash conf \rightsquigarrow conf' $$

Note that the WEBI transition relation has two parameters that model the transition. The first parameter is the *world oracle* wo, and the second one is `ε`, a list of all the possible physical events that might happen in the world. Regarding the wo, it is a function modeling the world. This function provides a new event happening in a particular context. The parameters of this function are the world's events log `L` and the `ε`, producing a physical event `pe` happening at a specific time `t`.

### 5.2.2.2 Client-Driven Rules

**ServiceInit.** The first rule we present is the `ServiceInit`. This rule instantiates a booting client and its related booting service picking an element from the set `I`. We present it in Figure 5.1.

Given an initializer, the rule resolves the URL via the function `WebServices`, returning a couple (`serviceinit`, `h`). The `serviceinit` is the *service initializer*, and `h` is the hostname of the host providing the service. The function application `serviceinit(v_a)` returns a service configuration `sc`, a program encoded in the service language and a fresh program memory, with a local variable `x` bound to `v_a`. The WEBI configuration is updated
ServiceInit

$$
\begin{array}{l}
\mathcal{I} = ((j, u), v_a) \cup \mathcal{I}' \quad \text{WebServices}(u) = (\text{serviceinit}, h) \\
\text{sc} = \text{serviceinit}(v_a) \quad \text{CC}' = \text{CC} \cup \{\langle \text{boot} \rangle^{(j,u)}\} \quad \text{SS}' = \text{SS} \cup \{\text{sc}^{((h,j),0)}\} \\
\text{wo}, \mathcal{E} \vdash \text{conf}\{\mathcal{I}, \text{CC}, \text{SS}\} \rightsquigarrow \text{conf}\{\mathcal{I}', \text{CC}', \text{SS}'\}
\end{array}
$$

Figure 5.1: The ServiceInit rule. A client is initialized. The booting call of this client generate a running web service.

accordingly. We write it as conf{I', CC', SS'}, meaning that the configuration conf mod-
ifies only the I, the CC, and the SS components.

We want to remark the id signing the booting service (((h, j), 0)). The i identifier
is explicitly set to 0. By convention, we set 0 as the callback identifier of the special
booting client callback boot.

In Figure 5.2, we present the Skel formalization of the ServiceInit rule. The evaluation function takes the world setting, an alias for the pair (wo, E), a WEBI configuration conf, and returns a configuration. We design the Skel WEBI configuration as a record. We present the type below.

type webiConfiguration = (
    _L_ : logEvents,
    _I_ : initializers,
    _HM_ : hostMemories,
    _SS_ : runningServiceConfigurations,
    _CC_ : webClientConfigurations,
    _IC_ : deviceConfigurations)

The body of the Skel term defines the rule. Thus, we get an element from the
initializers set. The pick function randomly chooses an element from I. It returns a
pair (((u,v_a), j), _I_, where the first element is an initializer, and the second is
I \ ((j, u), v_a).

Then, we define the webservices function as a mapping url -> (serviceInits, hostname).

The serviceInits is a function that, given a value, returns a service configuration.

Thus, similarly to the rule in Figure 5.1, we generate a service configuration sc and up-
```kotlin
1 type webClientConfiguration =
2 | Boot (identifier, url)
3 | Run ((webClient, callbacks, thunks) (identifier, url))
4
5 val evalServiceInit ((wo, _E):worldSetting)
6     (conf: webiConfiguration):
7         webiConfiguration =
8         let (((j,u),v), _I_) = pick<webClientBoot> conf._I_ in
9         let (serviceinit,h) = webservices(u) in
10        let sc = serviceinit(v) in
11        let _CC_ = _CC_add conf._CC_ (Boot (j,u)) in
12        let _SS_ = _SS_add conf._SS_ (sc, ((h,j),zero)) in
13        (conf <- (_I_ = _I_, _CC_ = _CC_, _SS_ = _SS_))
```

<caption>Figure 5.2: ServiceInit Skel rule.</caption>

date the WEBI configuration conf. To update a Skel record we use the following syntax:

```
(recordName <- (field1 = newValue))
```

On the left-hand side of the arrow, we have the record name (a variable named `recordName`), and on the right-hand side, we assign a new value (`newValue`) to a field (`field1`) only in the case we are actually updating it. The rest of the fields keep their old value. In Figure 5.2, we update only the fields related to *I*, *SS*, and *CC*. Note that on top of the figure, we present extensively the `webClientConfiguration`. The `Boot` constructor represents booting clients and the `Run` constructor represents the running ones.

**ClientStep.** The ClientStep rule describes what happens in the WEBI conf when a client performs a single evaluation step on its program. The client transition is parametrized by *C*, the client language semantics. We write this transition relation as $\rightsquigarrow_c$, relating a web-client configuration *cc* to another. To apply this rule, the client must be running.

In Figure 5.3, we present the small-step ClientStep rule. In Figure 5.4, we present the skeletal semantics of this rule. In line 10, we pick one of the running web clients from `_CC_r`, a partition of the `webClientConfigurations` *CC* containing only the clients
ClientStep

$$
\begin{align*}
CC &= \{\langle cc, B, T \rangle^{(j,u)}\} \cup CC' && cc = (P_c, \mu_c) \quad cc \rightsquigarrow C \quad cc' \\
CC'' &= \{\langle cc', B, T \rangle^{(j,u)}\} \cup CC' \\
wo, \mathcal{E} \vdash \text{conf}\{CC\} \rightsquigarrow \text{conf}\{CC''\}
\end{align*}
$$

<caption>Figure 5.3: The ClientStep rule. A web client performs an evaluation step.</caption>

1. `type clientStatus =`
2. | Ok
3. | NotifyCall (url, cl_val, (var, cl_stmt))
4. `type cl_out =`
5. | CL_Value cl_val
6. | CL_STMT (cl_stmt, clientStatus)
7. `val eval_CLIENTStep ((wo, _E_) : worldSetting)`
8. | (conf : webiConfiguration) :
9. | webiConfiguration =
10. | let (Run (((CL_STMT (cp, OK), mu_c), _B_, _T_), (j, u)), _CC_r') =
11. | | pick<webClient> conf._CC._CC_r in
12. | let cc' = eval_client cp mu_c in
13. | let _CC_'' = _CC_add (conf._CC_ <- (_CC_r = _CC_r'))
14. | | (Run (((cc', _B_, _T_), (j, u))), in
15. | (conf <- (_CC_ = _CC_''))

<caption>Figure 5.4: ClientStep Skel rule.</caption>

that have to step. Note that we edulcorate the semantics, by designing and using the
constructed **type webClientConfiguration**—presented in Figure 5.1)—for respectively
saying that a client is booting—⟨boot⟩<sup>(j,u)</sup>—or running—⟨cc, B, T⟩<sup>(j,u)</sup>. The picked ele-
ment signals the evaluation function whether the client can or cannot step. Note that on
top of the figure we show the **type clientStatus**. In this rule we show, after the pattern
matching, that the web client has a signal **Ok** stored in the **webClientConfiguration**.
This constructor is a signal meaning that the web client can step. The type constructor
**CL_STMT** is another signal, presented in the **type cl_out** definition, which signals that
the client still has something to compute. All the elements of **_CC_r** are web clients that
are programs (**CL_STMT**) that signal **Ok** to **WEBI**.
ClientCall

$$
\begin{align*}
CC &= \{\langle cc, B, T \rangle^{(j,u)}\} \cup CC' \\
cc \rightsquigarrow_C^{u'?!v_a, b^i} cc' \quad \text{WebServices}(u') = (\text{serviceinit}, h) \quad \text{sc} = \text{serviceinit}(v_a) \\
B' &= B \cup \{b^i\} \quad CC'' = \{\langle cc', B', T \rangle^{(j,u)} \cup CC'\} \quad SS'' = \{sc^{((h,j),i)}\} \cup SS \\
\frac{}{wo, \mathcal{E} \vdash \text{conf}\{CC, SS\} \rightsquigarrow \text{conf}\{CC'', SS''\}}
\end{align*}
$$

<caption>Figure 5.5: The ClientCall rule. A client calls a web service.</caption>

1. `val evalClientCall ((wo, _E_):worldSetting)`
2. `(conf:webiConfiguration):`
3. `webiConfiguration =`
4. `let (Run (((CL_STMT (cp, Notify (u', v_a, (b, i))), mu_c), _B_, _T_), (j, u)), _CC_c') = pick<webClient> conf._CC._CC_c in`
5. `let (serviceinit,h) = web services(u') in`
6. `let sc = serviceinit(v_a) in`
7. `let _B_` = `_B_add _B_ (b, i) in`
8. `let _CC_'' = _CC_add (conf._CC_ <- (_CC_c = _CC_c'))`
9. `(Run (((CL_STMT (cp, OK), mu_c), _B_', _T_'), (j, u))) in`
10. `let _SS_` = `_SS_add conf._SS_ (sc, ((h, j), i))) in`
11. `(conf <- (_CC_ = _CC_''`, `_SS_ = _SS_'))`

<caption>Figure 5.6: ClientCall Skel rule.</caption>

In line 12 of Figure 5.4, the client's program performs an evaluation step, and in line 13, the `_CC_` set is updated by first updating `_CC_r` with the partition without the picked `webClient (j,u)` ( `(conf._CC_ <- (_CC_r = _CC_r'))` ), and finally adding the new `webClientConfiguration` in `_CC_`. Finally, in line 15, we update the `webiConfiguration`.

ClientCall. A client calls a service. The call occurs on a client step that sends a value $v_a$ on a URL $u$ while preparing a handler $b$, signed with a unique callback identifier $i$. On the server-side, a service is ready to respond to this URL. We show the rule in Figure 5.5. A web client is picked from the partition set `_CC_c`, containing all the clients performing a call. Note that all the calling clients have `NotifyCall` as `clientStatus`. We show this in lines 4 and 5 of Figure 5.6. Then, similarly to the `ServiceInit` rule,
Run

$$ 
\begin{aligned}
CC &= \{ \langle \langle v'_c, \mu \rangle, B, \{ (\lambda x.P, v_c)^i \} \cup T \rangle^{(j,u)} \} \cup CC' \\
CC'' &= \{ \langle \langle (P\{x \mapsto v_c\}, \mu \rangle, B, T \rangle^{(j,u)} \} \cup CC' \\
&\qquad \text{wo, } \mathcal{E} \vdash \text{conf}\{CC\} \rightsquigarrow \text{conf}\{CC''\}
\end{aligned}
$$

<caption>Figure 5.7: The Run rule. When a client finishes to compute, it picks a chunk and executes it.</caption>

lines 6 and 7 create an instance of the service referenced by the URL u. In the Skel specification, we decided to evaluate with a client step the call construct of the client, producing a `webClientConfiguration` with the adequate `clientStatus`. This makes the implementation not represent the client relation $\rightsquigarrow^{u'v_a,b^i}$. Afterwards, we update the sets `_B`, `_CC`, and `_SS_` by adding the new callback $b^i$, the client with the `OK` status, and the new running web service signed by `((h,j),i)`. This web service is unique. Finally, in the last line, we return the updated `WEBI` configuration.

**Run.** A client finished computing, returning a value. If any, one of its chunks is picked, is put as the current client's code, and run. The client's memory stays unchanged. We show the rule in Figure 5.7. The Run only applies if a client has finished executing— returning a value—and has a chunk to be run.

In Figure 5.8, we show the skeletal semantics of this rule. We first pick a `WebClient` from `_CC_t`, if it exists. The latter is a partition of `_CC_` containing every client that finished computing and has a chunk ready to be executed or, in case of none, at least a callback. Then, we pick one of the chunks of the web client; we substitute the parameter of the callback program with the value stored in the chunk. Note that we discard the value returned by the client. Imagine that the value is the serialization of an HTML page. In that case, the result is local and meaningless regarding this orchestrating semantics. Finally, the set `_CC_` is updated, returning the new `WEBI` configuration. The implementation can fail in line 6, as the elements of `_CC_t` can have an empty set `_T_`. In this case, no client is ready to execute a chunk, as their callback still did not receive a value due to service execution.
```pascal
1 val evalRun ((wo, _E):worldSetting)
2 (conf:webiConfiguration):
3 webiConfiguration =
4 let (Run (((CL_Value _ , mu_c), _B_, _T_),(j,u)), _CC_t') =
5 pick<webClient> conf._CC._CC_t in
6 let (((x, _P_), v_c), _T_'), i) = pick<thunk> _T_ in
7 let _P_ = subst _P_ x v_c in
8 let _CC_'' = _CC_add (conf._CC_ <- (_CC_t = _CC_t'))
9 (Run (((CL_STMT (_P_', OK), mu_c), _B_, _T_'), (j,u))) in
10 (conf <- (_CC_ = _CC_''))
```

<caption>Figure 5.8: Run Skel rule.</caption>

### 5.2.2.3 Service-Driven Rules

**ServiceStep.** One of the running services makes an execution step; its host memory updates accordingly. We present the small-step rule in Figure 5.9. In the implementation depicted in Figure 5.10, we first use the usual `pick<a>` function to extract an element from the partition set of interests—`_SS_r`. In case of success, the element picked from `_SS_r` is a client that runs normally its code. Indeed, symmetrically with the client's partitioning, the `_SS_r` is a partition of `_SS_` containing all the running services that can step. The service picked is one that evaluates code different from an actuation or a get from a device. These two operations are designed as blocking operations in the Skel implementation. For being able to do a `ServiceStep`, we design a **type** `serviceStatus` stored in `sc` (lines 10 and 11) that must be either `Ok`, similarly to the client status type, or `GetDone v_s`. We allow the web services signed by `GetDone v_s` to step because this constructor means that the `get` operation finished successfully returning a result.

**ServiceStep**

$$ 
\begin{align*}
SS &= \{ \langle sc \rangle^{((h,j),i)} \} \cup SS' & \langle sc, HM(h) \rangle &\rightsquigarrow_S \langle sc', \mu'_h \rangle & HM' = HM[h \mapsto \mu'_h] \\
SS'' &= \{ \langle sc' \rangle^{((h,j),i)} \} \cup SS' & & & \\
wo, \mathcal{E} \vdash \text{conf}\{SS, HM\} &\rightsquigarrow \text{conf}\{SS'', HM'\}
\end{align*}
$$

<caption>Figure 5.9: The ServiceStep rule. A service performs an evaluation step.</caption>
The service step in this case acts for communicating to the service the value `v_s`. We show the `serviceStatus` on top of the listing—**type serviceStatus**.

The `_SS_add` function adds the `runningServiceState` to the correct partition of `_SS_`. In line 12 of Figure 5.10, we get the host memory `mu_h` and perform a single server evaluation step. The parameters are the server computation `sc`, the local memory `mu ls`, and the host memory `mu_h`. The result of the evaluation step is a triple with a new server computation `sc'`, local memory `mu ls'`, and host memory `mu_h'`. Finally, the host memories map `_HM_` and the set `_SS_` are updated, returning the new `WEBI` configuration.

**RetServiceBoot** and **RetService**. One server reaches a state where its code returns an immediate serialized value while the associated client is already running and has some handler ready to take a response; the handler becomes a chunk after interpretation of the serialized value response by the server. We remove this service from the `WEBI` configuration. Two rules depend on the client's state, whether a booting client or a running one. First, we discuss the rule for booting clients, depicted in Figure 5.11. Once the service related to a booting client converges to a value, the special callback

```kotlin
1  type serviceStatus =
2    | Ok
3    | ActCall (sr Actuator, sr DeviceID, sr Permission)
4    | GetCall (sr DeviceID, sr Permission)
5    | GetDone sr_val
6
7  val evalServiceStep ((wo, _E_):worldSetting)
8    (conf: webiConfiguration):
9      webiConfiguration =
10     let (((sc, mu ls), ((h, j), i)), _SS r') =
11       pick<runningServiceState> conf._SS_.SS r in
12     let mu_h = _HM_r(conf._HM_, h) in
13     let ((sc', mu_h'), mu ls') = eval_server sc mu_h mu ls in
14     let _HM_ = _HM_w(conf._HM_, h, mu h') in
15     let _SS_'' = _SS_add (conf._SS_ <- (_SS_r = _SS_r'))
16       ((sc', mu ls'), ((h, j), i)) in
17     (conf <- (_HM_ = _HM_', _SS_ = _SS_''))
```

<caption>Figure 5.10: ServerStep Skel rule.</caption>
RetServiceBoot

$$
\begin{align*}
SS &= \{\langle v_s \rangle^{((h,j),0)}\} \cup SS' \\
CC &= \{\langle \text{boot} \rangle^{(j,u)}\} \cup CC' \qquad \text{gencc}(v_s) = cc \qquad CC'' = CC' \cup \{\langle cc, \emptyset, \emptyset \rangle^{(j,u)}\} \\
\frac{}{\text{wo, } \mathcal{E} \vdash \text{conf}\{SS, CC\} \rightsquigarrow \text{conf}\{SS', CC''\}}
\end{align*}
$$

<caption>Figure 5.11: The RetServiceBoot rule. A service related to a booting client finishes to compute. It returns the result to the client.</caption>

boot becomes the actual value returned by the service. We assume that a service always returns code to a booting client. The function gencc takes the service execution result as a parameter and generates a client configuration. The rule is abstract enough to hide information about a possible client's local memory.

In Figure 5.12, we show the semantics in Skel. In this case, we choose to be more precise in defining how to generate the first running client signed by j and u. First, we pick a service that has finished executing from the partition set _SS_e (lines 4 and 5). This subset contains all the services that have finished computing.

In line 6 the booting client signed by j is extracted from _CC_. The function pick_by_j is a specialized function that looks for a client by identifier. Afterwards, we use the parsing function gencc to transform the server value result into a client program. This emulates the fact that in a web application, the server sends an HTML page which will be parsed and executed—for example, the JavaScript parts-on the client side—browser. The client program generation happens in line 7; the web client configuration is completed by a fresh new client memory and two empty sets, one of the callbacks and the other of thunks. Finally, we update the set _CC_ and return the final WEBI configuration. Note that we discard the service (h, j). This rule fails if a service returns a value to a booting client.

If the client is a running web client, things go slightly differently. First, services return values to the clients (pure values). Note that the URL u signing the client never changes. We present the rule for running clients in Figure 5.13. In this case, the value $v_s$ returned by the service $((h, j), i)$ is transformed into a client value $v_c$. It is associated with the callback $b^i$ of the client j waiting for that result. The callback becomes a thunk, as it can now be associated with a client value, represented as a pair $(b, v_c)^i$. The Skel code goes straightforward with what we did for the booting case but is consistent
<figure><img src="image_25.png" /><figcaption>Figure 5.12: RetServiceBoot Skel rule.</figcaption></figure>

### RetService

$$ 
\begin{aligned}
SS &= \{ \langle v_s \rangle^{(h,j),i} \} \cup SS' && CC = \{ \langle cc, B \cup \{b^i\}, T \rangle^{(j,u)} \} \cup CC' \\
gencc(v_s) &= v_c && CC'' = CC' \cup \{ \langle cc, B, T \cup \{(b, v_c)^i\} \rangle^{(j,u)} \} \\
\hline
\mathit{wo}, \mathcal{E} \vdash \mathit{conf}\{SS, CC\} \rightsquigarrow \mathit{conf}\{SS', CC''\}
\end{aligned}
$$

Figure 5.13: The RetService rule. A service realted to a running client finishes to compute. It returns the result to the client.

with the RetService rule. We show it in Figure 5.14. This rule fails in case the service returns some code to the client.

### 5.2.2.4 Device-driven Rules

**DeviceSensor.** A device or a group of devices detects a physical event from the world. This physical event is stored in the world log $\mathcal{L}$. To model the sensor detection, we use the world oracle wo. It takes the world log $\mathcal{L}$ and the set of possible events $\mathcal{E}$, and it forecasts a physical event pe at a particular time $t'$. The notion of time we use is discrete, providing an order to the different logs in $\mathcal{L}$. The new physical event and the time it happens are stored in the log. We present the small-step rule in Figure 5.15, and provide the Skel implementation in Figure 5.16. In Skel, we first produce a physical
<figure><img src="image_26.png" /><figcaption>Figure 5.14: RetService Skel rule.</figcaption></figure>

DeviceSensor

$$
\frac{\text{last-time}(\mathcal{L}) \le t' \quad \text{wo}(\mathcal{L}, \mathcal{E}, t') = pe \quad \text{IC} \rightsquigarrow_D^{\text{sens}(pe)} \text{IC}'}{\mathcal{L}' = (pe, t') :: \mathcal{L}}
$$

<caption>Figure 5.15: The DeviceSensor rule. A sensor, or a group of sensors detects a physical event.</caption>

event pe at a specific time t. We could use the Skel existential construct to produce a
time t' that satisfies last-time(\(\mathcal{L}\)) \le t', meaning that t' is the present. We decided to
rely on the implementation of the world oracle to produce this parameter. Then we per-
form a transition on the device semantics, add the new physical event to the list \(\mathcal{L}\), and
update the WEBI configuration. We remark that the eval\_device evaluation function is a
parameter of the model. Hence we decide to leave it dependent on the implementation
for now. In the current language example, this transition inspects the devices' memory
returning the physical event resulting from these readings.

We remark that this rule always applies and is independent of service calls such
as get or act. Notice that the difference between sensing and getting a value is that
the first only logs the resulting physical event in the L list, while the result of a get is
returned to a web service.
```pascal
1 val evalDeviceSensor ((wo, _E_):worldSetting)
2 (conf:webiConfiguration):
3 webiConfiguration =
4 (*we do not use last-time*)
5 let (pe,t') = world wo(conf._L_, world._E_) in
6 let (_IC_,'_,_) = eval_device conf._IC_ (DV_Sens pe) in
7 let _L_' = list_add<logEvent>(conf._L_, (Log_PE (pe,t')))) in
8 (conf <- (_L_ = _L_',_IC_ = _IC_'))
```

<caption>Figure 5.16: DeviceSensor Skel rule.</caption>

DeviceActuator

$$
\begin{align*}
SS &= \{\langle sc \rangle^{((h,j),i)}\} \cup SS' \\
\langle sc, HM(h) \rangle &\rightsquigarrow_S^{\text{act}(a,d,p)} \langle sc', \mu'_h \rangle \qquad HM' = HM[h \mapsto \mu'_h] \qquad IC \rightsquigarrow_D^{\text{act}(a,d,p)} IC' \\
SS'' &= \{\langle sc' \rangle^{((h,j),i)}\} \cup SS' \qquad \text{last-time}(\mathcal{L}) \le t' \qquad \mathcal{L}' = (a, d, t') :: \mathcal{L} \\
\text{wo, } \mathcal{E} \vdash \text{conf}\{\mathcal{L}, SS, HM, IC\} &\rightsquigarrow \text{conf}\{\mathcal{L}', SS'', HM', IC'\}
\end{align*}
$$

<caption>Figure 5.17: The DeviceActuator rule. A service issues an actuation order to a device. The device performs the actuation.</caption>

**DeviceActuator.** A service orders a device *d* to do an action *a* with permission to-ken *p*. To act, the device of name *d* should have the action *a* in its allowed actions set. Moreover, the permission *p* token should hold. While acting, the device's state is updated, and the action is recorded in the world state. The relation $IC \rightsquigarrow_D^{a,d,p} IC'$ does precisely that. The actual/concrete actuation cannot happen if one of these re-quirements does not hold. In Figure 5.18, we show the Skel implementation of the small-step rule presented in Figure 5.17. In the lastfigure, we implement the premises of the rule straightforwardly. First, we pick a service from the _SS_a partition set, which contains web services requesting an actuation to a device. Then we apply the device transition relation. Finally, we update the WEBI's sets _SS_, produce a discrete actua-tion time *t'*, and add the log to the world log _L_. We update the WEBI configuration accordingly. Note that we use a similar approach to the one used for the ClientCall, not performing the service transition but changing the serviceStatus from ActCall to Ok. We design the act as a blocking operation in the service language, and changing
```k
1 val evalDeviceActuator ((wo, _E_):worldSetting)
2     (conf:webiConfiguration):
3     webiConfiguration =
4     let (((SR_STMT (sc, ActCall (a,d,p)), mu ls), ((h, j), i)), _SS_a') =
5         pick<runningServiceState> conf._SS._SS_a in
6     let _IC_ = eval_device conf._IC_ (DV_Act (a,d,p)) in
7     let _SS_'' = _SS_add (conf._SS_ <- (sr_act = _SS_act))
8         ((SR_STMT (sc, SR_OK), mu ls), ((h, j), i)) in
9     let t' = last_time(conf._L_) in
10    let _L_ = list_add<logEvent> (conf._L_, (Log_Act (a,d,t')))) in
11    (conf <- (_L_ = _L_', _SS_ = _SS_'' , _IC_ = _IC_'))
```

<caption>Figure 5.18: DeviceActuator Skel rule.</caption>

DeviceReading

$$
\begin{align*}
SS &= \{ \langle sc \rangle^{((h,j),i)} \} \cup SS' & \langle sc, HM(h) \rangle &\rightsquigarrow_S^{\text{get}(d,p,v_a)} \langle sc', \mu_h' \rangle \\
IC &\rightsquigarrow_D^{\text{get}(d,p,v_a)} IC' & HM' &= HM[h \mapsto \mu_h'] & SS'' &= \{ \langle sc' \rangle^{((h,j),i)} \} \cup SS' \\
wo, \mathcal{E} \vdash & \text{conf}\{SS, HM, IC\} &\rightsquigarrow & \text{conf}\{SS'', HM', IC'\}
\end{align*}
$$

<caption>Figure 5.19: The DeviceReading rule. A service issues an reading order to a device. The device responds, returning a serialized value.</caption>

the status allows the service to step again.

**DeviceReading.** A web service requests a value stored in a device's memory. Similarly to the DeviceActuator rule, the service must have the correct permission *p* to perform this operation. The device reading happens if all these requirements are satisfied. We show the small-step rule in Figure 5.19.

In the implementation, presented in Figure 5.20, after picking a service requesting a `get`, an element of the partition set `_SS_g` (status `GetCall`), we perform a device transition issuing the order of reading the memory of the device `d`. The result of the step in line 6 is a pair `(_IC_', VSome v_a)`, where `IC_` is the new `deviceConfigurations` set, and `v_a` is the serialization of the read value. We do not make the service step, and again we manipulate the computation status from `GetCall` to `GetDone v_a`, the constructor designed to notify the service of the result of the device reading.
```kml
1  val evalDeviceReading ((wo, _E_):worldSetting)
2    (conf:webiConfiguration):
3    webiConfiguration =
4    let (((SR_STMT (sc, GetCall (d,p)), mu ls), ((h, j), i)), _SS_g') =
5      pick<runningServiceState> conf._SS_. _SS_g in
6    let (_IC_, v_a) = eval_device conf._IC_ (DV_Get (d,p)) in
7    let _SS_'' = _SS_add (conf._SS_ <- (_SS_g = _SS_g'))
8      ((SR_STMT (sc, GetDone v_a), mu ls), ((h, j), i)) in
9    (conf <- (_SS_ = _SS_'' , _IC_ = _IC_'))
```

<caption>Figure 5.20: DeviceReading Skel rule.</caption>

### 5.2.2.5 The Evaluation Function

In the introduction of the section we mentioned how easy would have been to implement a non-deterministic scheduling policy for WEBI. Without digging into the client, server and device language instantiation, in this subsection we present how to straightforwardly implement WEBI in Skel.

While introducing Skel in Chapter 2, we discussed about the interpretation monad and the way we deeply embedd the Skeletal Semantics in OCaml via the `necroml` tool. Hence, because of the definition of Skel [8], we can provide different interpretations to our specification language, delagating the bahaviour to the interpreter monad. We are interested in two behaviors. The first one is to have a monad that defines a non-deterministic (actually pseudo-randomic) semantics to the `branch` construct. Each time the `branch` is evaluated we want that the list of branches shuffles. In this way we do not know a priori which is the head of the branch list. Then, we are interested to exploit the collecting semantics behavior of the Skeletal semantics, collecting all the possible successful executions. The latter is a first technique that paves the way to formal analysis.

In Figure 5.21 we present the pseudo-random interpreter monad. From the figure we see the `Rand` module expecting another interpreter monad definition as a parameter. For example, if we provide the identity monad `ID` presented in Figure 2.5, the behavior of the latter monad would be changed only when dealing with branches, not evaluating anymore sequentially the list of branches. In the following snippet we show the actual instantiation of this monad.
```python
1 let shuffle l =
2     let () = Random self_init () in
3     let lrand = Stdlib.List.map (fun c ->
4         (Random.bits (), c)) l in
5     Stdlib.List.sort compare lrand |> Stdlib.List.map snd
6
7 module Rand (M: MONAD) = struct
8     include M
9     let branch l =
10         branch (shuffle l)
11 end
```

<caption>Figure 5.21: The pseudo-random interpretation monad</caption>

```python
1 open Necromonads
2 module IDRand = Necromonads.Rand(Necromonads.ID)
```

The file `Necromonads.ml`<fnref n="3" /> is the one containing some predefined interpretation monads provided with the `necrom` tool. To instantiate the collecting semantics behavior, we have a list monad which collects all the possible valid execution paths. We show this in Figure 5.22.

To write the actual evaluation function of `WEBI` in `Skel`, we just need to write a branch, each case having one of the rule's evaluation function. We present its structure in Figure 5.23. The code presented is pretty trivial. The `terminateWEBI`, is a function that exploits the aforementioned termination conjecture, stopping the `WEBI` evaluation as soon as no client is active. Otherwise, the model would work forever, ending a enu-merable number of infinite traces, because of the `DeviceSensor` rule. The latter always apply producing a physical event added to the world log list $\mathcal{L}$. Concerning the inter-est we have towards this model, we think that whatever happens after the termination conjecture is not of our interest.

<footnote n="3">3. https://gitlab.inria.fr/skeletons/necro-ml/-/blob/master/necromonads.ml</footnote>
```pascal
module List = struct
  type 'a t = 'a list
  let ret x = [x]
  let branch l =
    Sstdlib.List.concat (Sstdlib.List.map (fun f -> f()) l)
  let fail _ = []
  let rec union_two l = function
    [] -> l
    a :: q -> (if Sstdlib.List.mem a l then (fun x -> x)
                   else (Sstdlib.List.cons a)) (union_two l q)
  let rec union = function
    [] -> []
    a :: q -> union_two a (union q)
  let bind l f = union (Sstdlib.List.map f l)
  let apply f x = f x
  let extract x =
    begin match x with
      a :: _ -> a
      [] -> failwith "No result"
    end
end
```

<caption>Figure 5.22: The List interpretation monad</caption>

Remark

The non-deterministic concrete interpretation uses the `IDRand` module.ª

a. https://gitlab.inria.fr/skeletons/webi-in-skel/-/tree/master/semantics/webi

Remark

We exploit the termination conjecture to stop executing the model. If there are no clients and services manipulating the state of the world, then the physical events produced by the `DeviceReading` would be always the same. We deal with finite traces.
```pascal
1  val eval_WEBI ((wo,_E_):worldSetting)
2      (conf:webiConfiguration):
3      webiConfiguration =
4  branch let T = terminateWEBI conf in conf
5  or      let F = terminateWEBI conf in
6  let conf' =
7      branch eval_ServiceInit (wo,_E_) conf
8      or      eval_CLIENTStep (wo,_E_) conf
9      or      eval_CLIENTCall (wo,_E_) conf
10     or      eval_RUN (wo,_E_) conf
11     or      eval_ServiceStep (wo,_E_) conf
12     or      eval_RetServiceBoot (wo,_E_) conf
13     or      eval_RetService (wo,_E_) conf
14     or      evalDeviceSensor (wo,_E_) conf
15     or      evalDeviceActuator (wo,_E_) conf
16     or      evalDeviceReading (wo,_E_) conf
17  end in
18  eval_WEBI (wo,_E_) conf'
19 end
```

<caption>Figure 5.23: ServiceInit Skel rule</caption>

### 5.2.3 Example: The Cost of Non-Determinism

This section presents a simple example of how our model executes. We want to initialize `WEBI` with one client, two services, and three devices that can interact. To initialize the model, we need to provide semantics in Skel for both the client and server language. As mentioned and linked in the introduction, these languages are variants of the `While` language presented in Chapter 1.

The client language is a `While` language extended with a call statement for calling web services. The server language is more complex than the client's. For the sake of simplicity, we describe the language as an extension of a `While` language with an `act` and `get` statements, and a special expression `~`. The `act` and the `get` are statements to interact with devices. The tilde expression is of the form `~(p)`, where `p` is a program written in the client language syntax. The program `p` may contain special variables—called `$-variables`. These variables bind variable names to values in the server memory. The whole `~(program)` expression produces a server value—in the server semantics—with `$-variables` occurrences resolved. For the client, this server value is a program to
be. The Skel semantics of these languages must be included on top of the WEBI source,
using the keyword include. Thus, it is simple to write the WEBI semantics parametrized
by the tiers languages. A limitation is that all the interpreters generated by the necroml
tool need to use the same interpretation monad because of the bind function. Indeed,
to bind different computations produced by the three interpreters means to extrapolate
different notions of pure values and pass them to the continuations.<fnref n="4" />

5.2.3.1 Initial WEBI Configuration Setting

To provide an initial setting to the model, we introduce in the following paragraphs
how we define the two services, the client, the definition of the three devices, and the
definition of the two WEBI parameters: the world oracle wo and the set of the possible
events _E_. Afterward, we show how this model executes, discussing its strengths and
limitations.

Services. We define two services, one for handling the kitchen's window—opening or closing it—depending on the temperature in the room, and the other for turning on and off a connected oven in the same room. For example, a simple interaction of the oven with the kitchen's environment is to heat the room. We show the code of the two services, respectively, in Figures 5.24 and 5.25.

<footnote n="4">4. A concrete example is binding the resulting computation of the ID monad with the List one.
Binding a pure value—an integer, for example- is different from binding a list of results—which is the
pure value type for the latter monad.</footnote>
1 (x,
2 i = 0;
3 get(t, ("Thermometer", "kitchen"), "A");
4 while (i <= x) {
5 if (t > 26) {
6 act("open", ("Window", "kitchen"), "B");
7 } else {
8 act("close", ("Window", "kitchen"), "B");
9 };
10 i = i + 1;
11 get(t, ("Thermometer", "kitchen"), "A");
12 };
13 return ~ (return $t)
14 )

<caption>Figure 5.24: The windowManager service definition.</caption>

1 (,
2 act("on", ("Oven", "kitchen"), "C");
3 return ~ (return true)
4 )

<caption>Figure 5.25: The turnOnOven service definition.</caption>

1 (c,
2 i = 0;
3 while (true) {
4 get(presence, (("presenceSensor", "appt256"), 'A'))
5 if (presence = "present") {
6 act("on", ("switch", "appt256"), "B");
7 act("unlock", ("door", "appt256"), "C");
8 } else {
9 act("off", ("switch", "appt256"), "B");
10 act("lock", ("door", "appt256"), "C");
11 get(time, (("clock", "appt256"), "D")); (*not sure*)
12 if (time >= 800 & time <= 1800) then {
13 act("sendSMS", ("phone", "appt256"), "E")
14 (*Extend Webi ACT with param*)
15 }})
We say that a service is defined by a couple (var, sr_stmt), where var is a free variable in the program of type sr_stmt. The program is written according to the syntax of the server language. The windowManager service executes for a number x of iterations, given as a parameter by the caller. Each iteration of the service gets the temperature from a connected thermometer. Then, if the temperature is higher than 26°C, it opens. The program returns the final temperature got from the thermometer. Note that act has as parameters: an action a, a device identifier d—i.e. ("Window", "kitchen")-, and a permission token p. The turnOnOven service only turns on the oven and returns true.

Each service is identified by an url and a hostname of the machine on which this service executes. We write them below.

1 let windowManagerUrl = "windowManager.com/kitchen"

2 let hostWindowManager = "HostA"

3 let turnOnOvenUrl = "turnOnOven.com/kitchen"

4 let hostTurnOnOven = "HostB"

**Client.** We define one client: a client wanting to use the windowManager service to handle the window behavior automatically. While instantiating the model, these clients are initializers of the WEBI configuration. The client is an initializer of the initial WEBI configuration. We show the definition of the client and the initializer set _I_ instantiation in Figure 5.26. Note that a client's browser call is written as windowmanager.com/kitchen?x=1, where ?x=1 is the way to pass the parameter via a url. This parameter represents the number of iterations the windowManager will perform. To define _I_, we simply add the client to a list, the concrete type to implement sets.

**Devices.** We define three devices: the window, the thermometer, and the oven. We show how we design the window, then the others follow. To simplify, we design the device semantics as a record containing the operations that it offers and the device

1 let client = ("adam", "windowmanager.com/kitchen"), Some 1)

2 let _I_ = [client]

<caption>Figure 5.26: Definition of a client calling the windowManager and the _I_ set.</caption>
```c
1   type dv_step = ( device : deviceName,
2                  _GET_ : option<deviceMemory -> dv_val>,
3                  _ACT_ : option<deviceMemory -> actuator -> deviceMemory>,
4                  _SENS_ : option<deviceMemory -> dv_val -> deviceMemory>)
```

<caption>Figure 5.27: Type defining the device's semantics.</caption>

```c
1   val window_step : dv_step =
2     (device = "window",
3      _GET_ = (Some<deviceMemory -> dv_val>
4                (λ mu_d:deviceMemory -> dv_mem_get(mu_d, "window_status")))
5      _ACT_ = (Some<deviceMemory -> actuator -> deviceMemory>
6                (λ mu_d:deviceMemory -> λ a:actuator ->
7                 branch let DV_T = str_eq(a, "window open") in
8                  dv_mem_set(mu_d, window_status, (Bool T))
9                 or let DV_T = str_eq(a, "window close") in
10                dv_mem_set(mu_d, window_status, (Bool F))
11              end)),
12      _SENS_ = None<deviceMemory -> dv_val -> deviceMemory>)
```

<caption>Figure 5.28: The window semantics. The code is written in a simplified version of Skel, which has, for example, strings.</caption>

name. Figure 5.27 shows the Skel type definition of the structure containing the device semantics. The three operations we consider are `get`, `act`, and `sens`. The three fields are optional, meaning that devices might have only some of them defined. For example, a thermometer does not act. We show the actual implementation of the semantics of the window in Figure 5.28. The window has two actuators—`window_open` and `window_close-` and we handle them in the `_ACT_` field of the figure. We simply say that if the actuation is `"window open"`, the memory is updated to accordingly opening it; otherwise, to close it. The device's memory is a mapping from variables to device values. We store in the memory only one variable called `window_status`, which stores the actual status of the window. Because the window has no sensors, we set the `_SENS_` field to `None`. We define the `_GET_` to read the memory and return a value. We create the device's instance `kitchen_windows` in the following listing.
```c
1 (*Semantics*)
2 val thermometer_step :dv_step =
3     (device = "thermometer",
4      _GET_ = (Some<deviceMemory -> dv_val>
5               (λ mu_d:deviceMemory -> dv_mem_get(mu_d, "temp"))),
6      _ACT_ = None<deviceMemory -> actuator -> deviceMemory>,
7      _SENS_ = (Some<deviceMemory -> dv_val -> deviceMemory>
8               (λ mu_d:deviceMemory -> λ v:dv_val ->
9                 dv_mem_set(mu_d, "temp", v))
10     )
```

```c
1 (*Instantiation*)
2 (state = thermometer_init_memory(),
3 _S_ = ["temp"],
4 _A_ = [],
5 perm = "A",
6 id = ("thermometer", "kitchen"))
```

<caption>Figure 5.29: The thermometer semantics and instantiation.</caption>

```c
1 (state = window_init_memory(),
2 _S_ = [],
3 _A_ = ["window open", "window close"],
4 perm = "B",
5 id = ("Window", "kitchen"))
```

In detail, the term `window_init_memory` returns a fresh memory for the device, becoming the window's initial state. The state has only one binding, the name `window_status` bound to `closed`. The set of sensors `_S_` is empty, as none exists. The field `_A_` is a set of the permitted actuators for the device. The field `perm` contains the permission token, and the field `id` represents the device identifier `d`. The other device definitions follow the window's one. We show the thermometer in Figure 5.29, which features one sensor but no actuators. We define the semantics of the `_SENS_` operation in the semantics, updating the thermometer memory in the case of a `DeviceSensor`. The `_GET_` reads the device memory.
```kotlin
1 val wo ((L_, E_): (logEvents, list<event>)): (physicalEvent, time) =
2     let t' = log_time l in
3     branch let T = query_oven_kitchen_on l in
4         ((("thermometer", "kitchen"), Nat 28), t')
5     or
6         let F = query_oven_kitchen_on l in
7             ((("thermometer", "kitchen"), Nat 24), t')
8     end
9
10 type event =
11     | PE physicalEvent
11     | ACT actuator
```

<caption>Figure 5.30: The world oracle.</caption>

## World Oracle and Events.
We define these parameters of WEBI in Figure 5.30. The world oracle we describe is a function that returns the temperature depending on the state of the oven. Indeed, the oracle function inspects the oven's status, detecting `oven off` and returning the temperature of 24°C; otherwise, 28°C. This simple oracle models the influence of the oven on the environment in which it is placed. Notice that wo is a parameter of the semantics. Hence, one can design a more complex oracle, for example, one that models the physical world more accurately.

The `_E_` parameter is a set of events possible in the world we describe. This means that only the events defined in the `set_E_` can happen.

We define an *event* as a physical event or an actuator. A physical event represents the action of detecting a specific state in the world, and in Skel is represented by the type constructor `PE`. For example, the detection result of a thermometer can be `"At time t, the temperature of the kitchen is 28°C"`.

In Skel it is written as `PE ((("thermometer", "kitchen"), Nat 28), t)`. An actuator's action is a modification of the state of a device. An example is `"At time t, the kitchen's oven has been turned on"`. We represent it with the type constructor `ACT`, and we write the actuator action described before as `ACT ((("turn_on", ("thermometer", "kitchen")), t)`. We show the event type in Figure 5.30.
Initializing client "adam"

→ ServiceInit

Execution of the windowManager

→ ServiceStep → ServiceStep → DeviceSensor → DeviceReading → ServiceStep → ServiceStep → ServiceStep → ServiceStep → DeviceSensor → DeviceReading → ServiceStep

→ ServiceStep → ServiceStep

Returning the service result to the webclient "adam"

→ RetServiceBoot

Evaluating the result of the booting callback

→ ClientStep

Figure 5.31: A sequence of rule applications showing an execution of the initial setting presented in the previous paragraphs.

### 5.2.3.2 Execution

We are now ready to describe how the model executes. Concretely, we execute the initial configuration using the interpreter generated by the `necroml` tool, and the interpretation monad used is the `RandID`. Because of the evaluation function defined in Figure 5.23, we can theoretically obtain finite and infinite traces—for example, an infinite trace that contains an infinite number of `DeviceSensor` applications. As we test on a real interpreter, the interpreter quickly runs out of memory with this kind of trace.

**Execution 1.** Figure 5.31 presents an execution trace of the initial setting we previously defined. The figure shows a sequence of rule applications that reproduce the execution. For simplicity, we improperly refer to the sequences as traces. Hence, we consider a client, two services, and three devices. While booting, the client calls the `windowManager` service to handle the kitchen window. The first rule applied to the initial `WEBI` configuration is the `ServiceInit`. The client is a booting client whose related service is created and ready to execute. The booting call parameter of the client is the number 1, meaning that the service will perform only one iteration of the `windowManager`. This value is bound in the service's memory. At this point of the execution, only two rules can apply. The `ServiceStep` and the `DeviceSensor` rules. The trace we are considering applies the latter rule before each `get` or `act` interaction in the service code. Hence, after applying a service step, bounding the variable `i` to 0, the trace shows a `get`.

This changes the `serviceStatus` of the service to `GetCall` ("Kitchen", "window", "B"). As before, there are only two rules which
can be applied, the DeviceSensor and the DeviceActuator. The trace first does a DeviceSensor, adding to _L_ the physical event produced by the world oracle— ((("thermometer", "kitchen"), Nat 24), t')-and then applies a DeviceActuator. The temperature returned to the service is 24°C. This physical event is stored in the memory of the thermometer, accordingly to the _SENS_ rule presented in Figure 5.29. The physical event produced by the rule reflects the world's state: the oven is off. Afterward, the service keeps evaluating its code by applying the ServiceStep rule, evaluating the while and the if construct—with the related guards-. The second branch is evaluated, as the while's condition is satisfied, but not the if's. The case we are considering is when the temperature is ≤ 26°C. Because of the guard not satisfied, the else branch of the if statement is executed. Finally, a series of service steps evaluate the increment of the variable i, and a device sensor happens again before the get. The condition of the while is not satisfied anymore, so a series of service steps happen, evaluating the rest of the code and the return. The server expression ~ (return t) evaluates to (return (Nat 24)). Afterward, the RetServiceBoot rule is applied. It instantiates the running client, putting the service-generated program as the client's current program. After evaluating the return via a ClientStep, the WEBI evaluation function executes the term terminateWEBI, which is satisfied, returning the final WEBI configuration.

### Execution 2.
Now let us consider a variant of the initial setting, where we add a second client with permission tokens for interacting with the client's services in the previous setting. Indeed, we want the new client to call the `turnOnOven` service. We show the changes done to the initializers set `_I_` in the following snippet.

1. `let client1 = (("adam", "windowmanager.com/kitchen"), Some 1)`

2. `let client2 = (("steve", "turnonoven.com/kitchen"), None)`

3. `let _I_ = [client1, client2]`

Execution traces A and B are finite, like trace A presented in Figure 5.31. Both the traces first do two `ServiceInit` to introduce the booting clients and running services into the `WEBI` configuration. Then, the evolution of the traces is different. The trace A first consumes the steps of the `turnOnOven`, by doing a service step, a device sensor, and a device actuation which turns on the oven. Afterward, it consumes, similarly to the previous execution example, the service `windowManager`. The result of executing
Rule Sequence A.

Initializing client "adam" and "steve"

→ ServiceInit → ServiceInit

Execution of the turnOnOven service

→ ServiceStep → DeviceSensor → DeviceActuator → ServiceStep → ServiceStep

Returning the turnOnOven result to the webclient "steve"

→ RetServiceBoot

Execution of the windowManager service

→ ServiceStep → ServiceStep → DeviceSensor → DeviceReading → ServiceStep → ServiceStep → ServiceStep → DeviceSensor → DeviceActuator → ServiceStep → ServiceStep → DeviceSensor → DeviceReading → ServiceStep → ServiceStep → ServiceStep

Returning the windowManager result to the webclient "adam"

→ RetServiceBoot

Evaluating the result of the booting callbacks

→ ClientStep → ClientStep

Rule Sequence B.

Initializing client "adam" and "steve"

→ ServiceInit → ServiceInit

Execution of the windowManager service

→ ServiceStep → ServiceStep → DeviceSensor → DeviceReading → ServiceStep → ServiceStep → ServiceStep → ServiceStep → DeviceSensor → DeviceReading → ServiceStep → ServiceStep → ServiceStep

Returning the windowManager result to the webclient "adam"

→ RetServiceBoot

Execution of the turnOnOven service

→ ServiceStep → DeviceSensor → DeviceActuator → ServiceStep → ServiceStep

Returning the turnOnOven result to the webclient "steve"

→ RetServiceBoot

Evaluating the result of the booting callbacks

→ ClientStep → ClientStep

<caption>Figure 5.32: Two sequences of rule applications showing executions of the new setting that considers two clients. The first one is a trace showing an interaction producing an interesting physical event, and the second one does not show this interaction.</caption>

the latter service, differently from before, is to open the window, as the oven has been
turned on. This interaction between the two services and the related devices is indirect
and implicit. Indeed, the window actuation happens because of the temperature of the
kitchen raised by the oven, which is on. All the physical events and the actuations are
logged in _L_, and as we can see in the figure, result in the state of the window as
"window open". Trace B consumes the services the other way around by consuming all the execution steps of the windowManager and then consuming the turnOnOven ones. This results in not observing the interaction between the oven and the window, the one produced by the execution trace A.

**Discussion.** By using the RandID monad, we can only observe one trace of a non-deterministic execution of WEBI. Suppose we are now interested to collect all the possible traces produced by an initial WEBI configuration. Collecting all possible traces can be useful, for example, for detecting malicious behaviors. In theory we can use the List monad to make the Skel WEBI execution collect all possible traces, but this approach does not scale because of non-determinism—the interpreter runs out of memory.

This motivates the following section, a scheduler for WEBI, in which we stipulate under which hypotheses we can build an interpreter that collects all traces for a given initial WEBI configuration.

## 5.3 A Scheduler for WEBI

We propose a scheduled version of the WEBI semantics, which tames the non-determinism inherent in the model by defining an efficient order in which the WEBI rules are applied.

Section 5.3.1 presents the scheduler's semantics by introducing the hypotheses under which the scheduler semantics is equivalent to the non-deterministic semantics given in Section 5.1. Section 5.3.2 formally describes some properties the scheduler exploits to be equivalent to the non-deterministic semantics. Section 5.3.2.3 presents an equivalence proof sketch of the scheduler semantics concerning the observations made in the non-deterministic semantics. Finally, we conclude with Section 5.3.3, showing the example in Section 5.2.3 executed by the scheduler.

### 5.3.1 Semantics

To build the scheduler, we first discuss the shape of the scheduler's evaluation function. We draw two diagrams in Figure 5.33, one reflecting the behavior of the non-deterministic evaluation function depicted in Figure 5.23—which spans horizontally—and the other showing the behavior of the scheduler's evaluation function—which spans
vertically. We want to bind the non-deterministic behavior of the evaluation function by
providing an execution order to the rules that are not interdependent. Hence, commut-
ing two rules' applications does not change the produced WEBI configuration. In the
Skel code, if a branch fails, then another branch is picked for evaluation. Diagram B of
the figure graphically presents the scheduler's evaluation function.

The scheduler's first iteration consumes all the `ServiceInits` upfront to introduce
all the initializers of the configuration at once, emptying `_I_`. Afterward, the sched-
uler consumes all the `ServiceSteps`, elements of `_SS_r`. Once this partition is empty,
we know that the configuration might have services that have finished computing—
elements of `_SS_e-`, waiting to `act`—elements of `_SS_a-`, and waiting to `get`—elements
of `_SS_g`. The scheduler first handles the finished services, repeatedly applying the
`RetServiceBoot`, and creating the running web clients. Once the partition set of `_SS_—
_SSE` is empty, the scheduler consumes elements of the partitions `_SS_a` and `_SS_g`.
The current step makes the interaction between services and devices happen, if any.
We design this step of the scheduler to `act`, `get`, or to skip this step. If the scheduler
applies a device interaction rule, before applying it, performs a `DeviceSensor` to up-
date the devices' memories with the physical events generated by the world oracle. In
this way, the device memories reflect the status of the physical world. Otherwise, the
scheduler moves to the next step. Note that the scheduler can also move to the client-
driven rules if the partition sets `_SS_a` and `_SS_g` are empty. The next step consumes
all the elements of the partition set `_CC_r` by repeatedly applying the `ClientStep` rule.
Afterward, it consumes the client calls by repeatedly applying the `ClientCall` rule to
the elements of `_CC_c`. Finally, if any, it runs the thunks of the web clients elements of
 `_CC_t`.

Once all the elements of `_CC_t` are processed, the scheduler completes its first itera-
tion.

The successive iterations are slightly different. They do not do the `ServiceInit`
step, which applies the `RetService` or the `RetServiceBoot` rule depending on which
type of client the services are returning—booting or running.

5.3.1.1 Assumptions for the Scheduler

To tame the non-determinism, we must put constraints on the WEBI and tiers' semantics.
The following hypotheses allow us to prove the equivalence between the scheduler and
the WEBI non-deterministic semantics.
<figure><img src="image_27.png" /></figure>

<figure><img src="image_28.png" /><figcaption>Figure 5.33: Two diagrams representing the evaluation functions. The diagram A depicts the non-deterministic evaluation function, and the diagram B depicts the scheduler’s one.</figcaption></figure>
Concerning the server and client language, we assume that they rely on a deterministic semantics. Moreover, the services are concurrent, modifying the host memory of the server they are executing on. We assume that a running service never touches the host memory. We present these constraints in Hypotheses 1, 2, and 3.

**Hypothesis 1** Given a web service configurations *sc* and a host memory *μh*, two different executions result in the same final configuration.

$$ \forall \langle sc, \mu_h \rangle : \\ \quad (\langle sc, \mu_h \rangle \rightsquigarrow_S \langle sc', \mu'_h \rangle) \wedge \\ \quad (\langle sc, \mu_h \rangle \rightsquigarrow_S \langle sc'', \mu''_h \rangle) \Rightarrow (sc' = sc'' \wedge (\mu_h = \mu'_h)) $$

**Hypothesis 2** The client semantics is deterministic.

$$ \forall cc, cc', cc'' : (cc \rightsquigarrow_C cc') \wedge (cc \rightsquigarrow_C cc'') \Rightarrow (cc' = cc'') $$

**Hypothesis 3** Given a web service configurations *sc* and a host memory *μh*, executing one step of the semantics does not change the host memory.

$$ \forall \langle sc, \mu_h \rangle : \\ \quad (\langle sc, \mu_h \rangle \rightsquigarrow_S \langle sc', \mu'_h \rangle) \Rightarrow \\ \quad (\mu_h = \mu'_h) $$

To avoid ambiguity in choosing clients or services, we define two hypotheses concerning the uniqueness of the web services and web clients in a WEBI configuration. Every client and service running in a WEBI configuration is unique. We present these properties of the running model in Hypotheses 4 and 5.

**Hypothesis 4** Every running web service in a WEBI configuration is uniquely identified.

$$ \forall \langle sc \rangle^{((h,j),i)}, \langle sc' \rangle^{((h',k),l)} \in SS : \\ h = h' \wedge j = k \wedge i = l \Rightarrow \\ sc = sc' $$
**Hypothesis 5** Every web client in a WEBI configuration is uniquely identified.

$$ \forall cc^{(j,u)}, cc^{(j',u')} \in CC : $$

$$ j = j' \land u = u' \Rightarrow $$

$$ cc = cc' $$

### 5.3.1.2 Scheduler Configuration

We first introduce a set of labels to represent WEBI rules:

* SS is the label representing the ServiceStep. The label can hold indices $(j, i)$, written as $SS_{(j,i)}$, for making step the service identified by $(j, i)$.

* RS is the label representing either the RetService or RetServiceBoot. The label can hold indices $(j, i)$, written as $RS_{(j,i)}$, for making return the service identified by $(j, i)$.

* CS is the label representing the ClientStep. The label can hold an index $j$, written as $CS_j$, for making step the client identified by $j$.

* IN is the label representing the ServiceInit. The label does not hold indices.

* CC$_j$ is the label representing the ClientCall. The label can hold an index $j$, written as $CC_j$, for making call the client identified by $j$.

* RN is the label representing the Run. The label can hold indices $(j, i)$, written as $RN_{(j,i)}$, to run the chunk $i$ of the client identified by $j$.

* DS is the label representing the DeviceSensor. The label does not hold indices.

* DA is the label representing the DeviceActuator. The label can hold indices $(j, i)$, written as $DA_{(j,i)}$, for making a service $(j, i)$ issuing an actuation.

* DR is the label representing the DeviceReading. The label can hold indices $(j, i)$, written as $DR_{(j,i)}$, for making a service $(j, i)$ issuing a reading.

* DV is a generic device label. $DV \in \{DS, DA, DR\}$.
We add a special label `end` to signal that the `WEBI`'s scheduler has finished computing. We let $X$ range over labels, i.e. $X \in \{SS, RS, CS, IN, CC, RN, DS, DA, DR, DV, end\}$.

We define a scheduler transition as a relation between the scheduler's configurations. A scheduler configuration is an extended `WEBI` configuration enclosed in a scheduler's context $\llbracket \rrbracket$.

The `WEBI` configuration defined in Section 5.2.1 is extended with $\Pi$, written $\langle \mathcal{L}, \mathcal{I}, HM, SS, CC, IC, \Pi \rangle$, where $\Pi$ is a finite list of labels. Intuitively, the sequence $\Pi$ represents a `WEBI` execution trace and it will be useful for proving equivalence. We define in Definition 5 how an initial `WEBI` configuration is formed.

**Definition 5** A well-formed `WEBI` initial configuration, is a configuration $\langle \mathcal{L}, \mathcal{I}, HM, SS, CC, IC, \Pi \rangle$, where:

* Lists $\mathcal{L}$ and $\Pi$ are empty lists.

* Sets $SS$ and $CC$ are empty sets.

* Set $\mathcal{I}$ is a non-empty set of clients that are booting.

* Mapping $HM$ is a pre-instantiated map of host-memories hostname $\rightarrow$ hostmemory.

* Set $IC$ is a set of initial device configurations.

The scheduler context holds three parameters, a label representing a rule name— meaning the current scheduling step executing-and two filtering of the trace $\Pi$—one containing device rule applications and the other having the order of the Run rule applications. The two filterings ensure the execution of the scheduler semantics to reproduce a final `WEBI` configuration equivalent to the one produced by `WEBI`.

We can write a scheduling context configuration as $\llbracket \text{conf} \rrbracket_X$, with the $X$ denoting the generic scheduling step. For example, to write the scheduling step of the `ServiceStep` we write $\llbracket \text{conf} \rrbracket_{SS}$. Moreover, we use these labels to annotate the non-deterministic `WEBI` transition relation. Intuitively, $\rightsquigarrow_X$ keeps the abstraction of the model, and $\rightsquigarrow_{SS(j,i)}$ states the application of a service step on a web client signed by $(j, i)$.

**Device and Thunk Filterings.** We introduce two parameters which are lists of labels: $\mathcal{L}$ for the device rule applications and $\mathcal{T}$ for the Run rule applications. The purpose
Filtering Functions for Generating $\mathcal{L}$

$$ \pi_{\mathcal{L}} = \lambda\Pi. \mathit{lfilter} \Pi (\lambda x.x \in \{\mathit{DS}, \mathit{DA}, \mathit{DR}\}) $$

Filtering Functions for Generating $\mathcal{T}$

$$ \pi_{\mathcal{T}} = \lambda\Pi. \mathit{lfilter} \Pi (\lambda x.x \in \{\mathit{RN}\}) $$

Figure 5.34: Filtering functions on $\Pi$, where `lfilter` is the classic filter function on lists in functional programming.

is to drive the scheduler's execution and obtain a trace equivalent to the one produced by the non-deterministic execution of the model. Figure 5.34 presents the algorithms for generating the two execution guides, $\mathcal{L}$ and $\mathcal{T}$. We call the two filtering functions $\pi_{\mathcal{L}}$ and $\pi_{\mathcal{T}}$, which return a sub-trace given a trace $\Pi$.

**Scheduler Transition Relation.** We write the scheduler relation as $\rightsquigarrow_{\mathcal{G}}$. Thus, the relation between scheduler's configurations has the following form:

$$ wo, \mathcal{E} \vdash [\mathit{conf}]_{\mathcal{X}}^{(\mathcal{L}, \mathcal{T})} \rightsquigarrow_{\mathcal{G}} [\mathit{conf}']_{\mathcal{X}'}^{(\mathcal{L}', \mathcal{T}')} $$

### 5.3.1.3 Small-Step Semantics

We present the scheduler's semantics by presenting each step in a paragraph. Given an initial WEBI configuration `conf`, an initial configuration for the scheduling is $[\mathit{conf}]_{\mathit{IN}}^{(\mathcal{L}, \mathcal{T})}$, for some $\mathcal{L}$ and $\mathcal{T}$.

**Step 1, IN.** The first iteration of the scheduler starts evaluating all the initializers. This approach introduces all the booting clients and the related booting services. We show the semantic rules in Figure 5.35.

The rule `Init` performs a `ServiceInit` transition—Figure 5.1-in case the set $\mathcal{I}$ is not empty. Note that the left-hand side of the conclusions of the inference rule keeps the label `IN`, stating that the scheduler step does not change.
Step 1

$$ \frac{\mathcal{I} \neq \emptyset \quad wo, \mathcal{E} \vdash \text{conf}\{\mathcal{I}\} \rightsquigarrow_{\text{IN}} \text{conf}'}{wo, \mathcal{E} \vdash \left[\text{conf}\{\mathcal{I}\}\right]_{\text{IN}}^{(\mathcal{L}, \mathcal{T})} \rightsquigarrow_{\mathcal{E}} \left[\text{conf}^{\prime}\right]_{\text{IN}}^{(\mathcal{L}, \mathcal{T})}} $$

$$ \frac{\mathcal{I} = \emptyset}{wo, \mathcal{E} \vdash \left[\text{conf}\{\mathcal{I}\}\right]_{\text{IN}}^{(\mathcal{L}, \mathcal{T})} \rightsquigarrow_{\mathcal{E}} \left[\text{conf}\{\mathcal{I}\}\right]_{\text{SS}}^{(\mathcal{L}, \mathcal{T})}} $$

<caption>Figure 5.35: Semantic rules for Step 1</caption>

The rule InitDone makes the scheduler transit to the next step in case the set of initializers is empty. As we deal with a finite number initializing of clients, once the *I* set is emptied, it will not have new elements to initialize the next iteration. Step 1 of the scheduler is performed only at the first iteration. Note that this rule makes the scheduler transit to the second scheduler step by changing the label *IN* to *SS* in the context.

Step 2, *SS*. The second step of the scheduling policy consumes all the possible *ServiceSteps*. This means that each time the rule is applied, an element of *SS*<sub>*r*</sub> performs an execution step. The step finishes as soon as no more services can step. We present the semantics in Figure 5.36.

The *ServiceChosen* rule picks a service that can step and updates the scheduler. The rule label is set to context with *SS*<sub>*r*,*i*</sub>, meaning that the service (*j*, *i*) is the one chosen to step.

The *MultiServiceSteps* rule makes step the web service (*j*, *i*). If the service can do one more step, the label is left unchanged, updating only the configuration.

The *OneServiceStep* acts closely to the *MultiServiceStep* rule. The service performs one small evaluation step, and the rule label is set to *SS*. This means that the service (*j*, *i*) cannot step again. Another service has to be chosen or, in case, transit to the next scheduling step.

The *ServicesDone* rule makes the scheduler transit to the next scheduling step. Hence, the *SS*<sub>*r*</sub> partition set is empty, and the rule label changes to *RS*.

Generally, the running service executing on a host are concurrent, as they share the host memory. In this preliminary study of WEBI, we decided to put constraints, saying that the running services never touch the host memory. This permits the *MultiServiceStep* to be correct. Moreover, we constrain the server language and consider only deterministic languages. These constraints are formally presented in Hy-
Step 2

SERVICECHOSEN

$$
SS = \{SS_r, SS_a, SS_g, SS_e\}
$$

$$
SS_r \neq \emptyset \quad \langle sc \rangle^{((h,j),i)} \in SS_r
$$

$$
\text{wo, } \mathcal{E} \vdash \llbracket \text{conf}\{SS\} \rrbracket_{\text{SS}}^{\mathcal{L}, \mathcal{T}} \rightsquigarrow \mathcal{G} \quad \llbracket \text{conf}\{SS\} \rrbracket_{\text{SS}(j,i)}^{\mathcal{L}, \mathcal{T}}
$$

MULTISERVICESTEPS

$$
wo, \mathcal{E} \vdash \text{conf}\{SS\} \rightsquigarrow_{\text{SS}(j,i)} \text{conf}'{SS'}
$$

$$
SS' = \{SS_r, SS_a, SS_g, SS_e\} \quad \langle sc \rangle^{((h,j),i)} \in SS_r
$$

$$
\text{wo, } \mathcal{E} \vdash \llbracket \text{conf}\{SS\} \rrbracket_{\text{SS}(j,i)}^{\mathcal{L}, \mathcal{T}} \rightsquigarrow \mathcal{G} \quad \llbracket \text{conf}'\{SS'\} \rrbracket_{\text{SS}(j,i)}^{\mathcal{L}, \mathcal{T}}
$$

ONESERVICESTEP

$$
wo, \mathcal{E} \vdash \text{conf}\{SS\} \rightsquigarrow_{\text{SS}(j,i)} \text{conf}'{SS'}
$$

$$
SS' = \{SS_r, SS_a, SS_g, SS_e\} \quad \langle sc \rangle^{((h,j),i)} \notin SS_r
$$

$$
\text{wo, } \mathcal{E} \vdash \llbracket \text{conf}\{SS\} \rrbracket_{\text{SS}(j,i)}^{\mathcal{L}, \mathcal{T}} \rightsquigarrow \mathcal{G} \quad \llbracket \text{conf}'\{SS'\} \rrbracket_{\text{SS}}^{\mathcal{L}, \mathcal{T}}
$$

SERVICES DONE

$$
SS = \{SS_r, SS_a, SS_g, SS_e\} \quad SS_r = \emptyset
$$

$$
\text{wo, } \mathcal{E} \vdash \llbracket \text{conf}\{SS\} \rrbracket_{\text{SS}}^{\mathcal{L}, \mathcal{T}} \rightsquigarrow \mathcal{G} \quad \llbracket \text{conf}\{SS\} \rrbracket_{\text{RS}}^{\mathcal{L}, \mathcal{T}}
$$

<caption>Figure 5.36: Semantic rules for Step 2</caption>

potheses 3 and 1.

Step 3, RS. The third step consumes all the elements of SS_e, and only RetService
and RetServiceBoot apply.

We present the semantics in Figure 5.37.

The RetServiceChosen rule picks a service in SS<sub>e</sub>. This service is related to a boot-
ing or a running client. Hence, one of the two applies. The WEBI configuration is updated
accordingly.

The RetServiceDone rule makes the scheduler transit to the next step because of
$SS_g = \emptyset$. The rule label changes to DV. The WEBI configuration conf, L, and T are
immuted.
Step 3

$$
\begin{align*}
\text{RETSERVICECHOSEN} \\
SS &= \{SS_r, SS_a, SS_g, SS_e\} \\
SS_e &\neq \emptyset \quad \langle sc \rangle^{(h,j),i} \in SS_e \\
\text{wo, } \mathcal{E} \vdash \text{conf}\{SS\} &\rightsquigarrow_{\mathbb{RS}_{(j,i)}} \text{conf}'\{SS'\} \\
\text{wo, } \mathcal{E} \vdash &\llbracket \text{conf}\{SS\} \rrbracket_{\mathbb{RS}}^{\mathcal{L}, \bar{\mathcal{L}}} \rightsquigarrow_{\mathcal{G}} \llbracket \text{conf}'\{SS'\} \rrbracket_{\mathbb{RS}}^{\mathcal{L}, \bar{\mathcal{L}}} \\
\text{RETSERVICESDONE} \\
SS &= \{SS_r, SS_a, SS_g, SS_e\} \\
SS_e &= \emptyset \\
\text{wo, } \mathcal{E} \vdash &\llbracket \text{conf}\{SS\} \rrbracket_{\mathbb{RS}}^{\mathcal{L}, \bar{\mathcal{L}}} \rightsquigarrow_{\mathcal{G}} \llbracket \text{conf}\{SS\} \rrbracket_{\mathbb{DV}}^{\mathcal{L}, \bar{\mathcal{L}}}
\end{align*}
$$

<caption>Figure 5.37: Semantic rules for Step 3</caption>

Step 4, DV. The fourth step of the scheduler consumes all the services interacting with devices. We are considering the DS, DA, and DR rules, and trace L guides the application of these rules. We present the semantics in Figure 5.38.

The DevSens rule applies a DeviceSensor in case the head of the device-trace L is DS. The WEBI configuration conf is updated accordingly. Regarding the scheduler context, the new context contains the list L without its head, and the rule label stays unchanged.

The DevAct rule, if the head of the L is an actuator, applies the DeviceActuation rule to the WEBI configuration. The service requesting the act is (j, i), and must be an element of SS<sub>a</sub>. The WEBI configuration and the L are updated, and the rule label stays unchanged.

Similarly, the DevRead performs a DeviceReading requested by the service (j, i) in case the service belongs to SS<sub>g</sub>. The head of the L is removed, the configuration is updated, and the rule label does not change.

The DevNoAct and DevNoRead apply when respectively:

* The head of L is an actuator request done by a service (j, i), but the service is not an element of SS<sub>a</sub>.

* The head of L is a read request done by a service (j, i), but the service is not an element of SS<sub>g</sub>.
Step 4

$$ \mathcal{D}EV\mathcal{S}ENS \quad \mathcal{L} = \mathcal{D}S :: \mathcal{L}' \quad wo, \mathcal{E} \vdash \mathit{conf} \rightsquigarrow_{\mathcal{D}S} \mathit{conf}' \\ wo, \mathcal{E} \vdash [\mathit{conf}]_{\mathcal{D}V}^{\mathcal{L}, \mathcal{T}} \rightsquigarrow_{\mathcal{G}} [\mathit{conf}']_{\mathcal{D}V}^{\mathcal{L}', \mathcal{T}} $$

$$ \mathcal{D}EV\mathcal{A}CT \quad \mathcal{L} = \mathcal{D}A_{(j,i)} :: \mathcal{L}' \quad SS = \{SS_r, SS_a, SS_g, SS_e\} \\ \langle sc \rangle^{((h,j),i)} \in SS_a \quad wo, \mathcal{E} \vdash \mathit{conf}\{SS\} \rightsquigarrow_{\mathcal{D}A_{(j,i)}} \mathit{conf}'\{SS'\} \\ wo, \mathcal{E} \vdash [\mathit{conf}\{SS\}]_{\mathcal{D}V}^{\mathcal{L}, \mathcal{T}} \rightsquigarrow_{\mathcal{G}} [\mathit{conf}'\{SS'\}]_{\mathcal{D}V}^{\mathcal{L}', \mathcal{T}} $$

$$ \mathcal{D}EV\mathcal{R}EAD \quad \mathcal{L} = \mathcal{D}R_{(j,i)} :: \mathcal{L}' \quad SS = \{SS_r, SS_a, SS_g, SS_e\} \\ \langle sc \rangle^{((h,j),i)} \in SS_g \quad wo, \mathcal{E} \vdash \mathit{conf}\{SS\} \rightsquigarrow_{\mathcal{D}R_{(j,i)}} \mathit{conf}'\{SS'\} \\ wo, \mathcal{E} \vdash [\mathit{conf}\{SS\}]_{\mathcal{D}V}^{\mathcal{L}, \mathcal{T}} \rightsquigarrow_{\mathcal{G}} [\mathit{conf}'\{SS'\}]_{\mathcal{D}V}^{\mathcal{L}', \mathcal{T}} $$

$$ \mathcal{D}EV\mathcal{N}O\mathcal{A}CT \quad \mathcal{L} = \mathcal{D}A_{(j,i)} :: \mathcal{L}' \quad SS = \{SS_r, SS_a, SS_g, SS_e\} \quad \langle sc \rangle^{((h,j),i)} \notin SS_a \\ wo, \mathcal{E} \vdash [\mathit{conf}\{SS\}]_{\mathcal{D}V}^{\mathcal{L}, \mathcal{T}} \rightsquigarrow_{\mathcal{G}} [\mathit{conf}\{SS\}]_{\mathcal{CS}}^{\mathcal{L}, \mathcal{T}} $$

$$ \mathcal{D}EV\mathcal{N}O\mathcal{R}EAD \quad \mathcal{L} = \mathcal{D}R_{(j,i)} :: \mathcal{L}' \quad SS = \{SS_r, SS_a, SS_g, SS_e\} \quad \langle sc \rangle^{((h,j),i)} \notin SS_g \\ wo, \mathcal{E} \vdash [\mathit{conf}\{SS\}]_{\mathcal{D}V}^{\mathcal{L}, \mathcal{T}} \rightsquigarrow_{\mathcal{G}} [\mathit{conf}\{SS\}]_{\mathcal{CS}}^{\mathcal{L}, \mathcal{T}} $$

$$ \mathcal{D}EV\mathcal{S}TEP\mathcal{D}ONE \quad SS = \{SS_r, SS_a, SS_g, SS_e\} \quad \mathcal{L} = [] \Rightarrow (SS_a = \emptyset \land SS_g = \emptyset) \\ wo, \mathcal{E} \vdash [\mathit{conf}\{SS\}]_{\mathcal{D}V}^{\mathcal{L}, \mathcal{T}} \rightsquigarrow_{\mathcal{G}} [\mathit{conf}\{SS\}]_{\mathcal{CS}}^{\mathcal{L}, \mathcal{T}} $$

<caption>Figure 5.38: Semantic rules for Step 4</caption>

In this case, for keeping the device-rules application order, the rule makes the scheduler context transit to the next step to the scheduler. The rule label is set to CS.

Finally, The DevStepDone applies when the list $\mathcal{L}$ is empty. We know that if this trace is empty, then both the partition sets $SS_a$ and $SS_g$ are empty. This rule application only changes the rule label to CS.

Step 5, CS The fifth step handles the ClientStep application. We present the small-step semantics in Figure 5.39.
Step 5

$$
\begin{array}{l}
\text{CLIENTCHOSEN} \\
\quad CC = \{CC_r, CC_c, CC_t, CC_e\} \qquad CC_r \neq \emptyset \qquad cc^{(j,u)} \in CC_r \\
\quad \text{wo, } \mathcal{E} \vdash [\text{conf}\{CC\}]_{\mathcal{CS}}^{\mathcal{L}, \mathcal{T}} \rightsquigarrow \mathcal{E} [\text{conf}\{CC\}]_{\mathcal{CS}_j}^{\mathcal{L}, \mathcal{T}}
\end{array}
$$

$$
\begin{array}{l}
\text{MULTICLIENTSTEPS} \\
\quad \text{wo, } \mathcal{E} \vdash \text{conf}\{CC\} \rightsquigarrow_{\mathcal{CS}_j} \text{conf}'\{CC'\} \\
\quad CC' = \{CC_r, CC_c, CC_t, CC_e\} \qquad cc^{(j,u)} \in CC' \\
\quad \text{wo, } \mathcal{E} \vdash [\text{conf}\{CC\}]_{\mathcal{CS}_j}^{\mathcal{L}, \mathcal{T}} \rightsquigarrow \mathcal{E} [\text{conf}'\{CC'\}]_{\mathcal{CS}_j}^{\mathcal{L}, \mathcal{T}}
\end{array}
$$

$$
\begin{array}{l}
\text{ONECLIENTSTEP} \\
\quad \text{wo, } \mathcal{E} \vdash \text{conf}\{CC\} \rightsquigarrow_{\mathcal{CS}_j} \text{conf}'\{CC'\} \\
\quad CC' = \{CC_r, CC_c, CC_t, CC_e\} \qquad cc^{(j,u)} \notin CC_r \\
\quad \text{wo, } \mathcal{E} \vdash [\text{conf}]_{\mathcal{CS}_j}^{\mathcal{L}, \mathcal{T}} \rightsquigarrow \mathcal{E} [\text{conf}']_{\mathcal{CC}}^{\mathcal{L}, \mathcal{T}}
\end{array}
$$

$$
\begin{array}{l}
\text{CLIENTSDONE} \\
\quad CC = \{CC_r, CC_c, CC_t, CC_e\} \qquad CC_r = \emptyset \qquad |CC_e| \neq |CC| \\
\quad \text{wo, } \mathcal{E} \vdash [\text{conf}\{CC\}]_{\mathcal{CS}}^{\mathcal{L}, \mathcal{T}} \rightsquigarrow \mathcal{E} [\text{conf}\{CC\}]_{\mathcal{CC}}^{\mathcal{L}, \mathcal{T}}
\end{array}
$$

$$
\begin{array}{l}
\text{WEBIDONE} \\
\quad CC = \{CC_r, CC_c, CC_t, CC_e\} \qquad CC_r = \emptyset \qquad |CC_e| = |CC| \\
\quad \text{wo, } \mathcal{E} \vdash [\text{conf}\{CC\}]_{\mathcal{CS}}^{[1,1]} \rightsquigarrow \mathcal{E} [\text{conf}\{CC\}]_{\text{end}}^{[1,1]}
\end{array}
$$

<caption>Figure 5.39: Semantic rules for Step 5</caption>

The ClientChosen rule picks a client to step from the partition set $CC_r$. If there is a client $(j, u)$, the rule label is set to $\mathcal{CS}_j$.

The MultiClientSteps rule performs an execution step on the web client signed by $(j, u)$. The client, still a member of $CC_r$ in conf', is set again for evaluation. Hence, the rule label does not change, and the WEBI configuration is updated.

The OneClientStep rule performs an execution step on the web client (j, u). The client is no more in $CC_r$ of conf'. Hence, the rule label is set back to CC. The label change permits choosing another client to make an execution step, to go to the next scheduling step, or to terminate WEBI, according to Definition 2, page 128. The WEBI configuration is updated.

The rule ClientsDone applies if there are no more clients in the partition set $CC_r$.
Step 6

$$
\begin{array}{l}
\text{CALLCHOSEN} \\
\quad CC = \{CC_r, CC_c, CC_t, CC_e\} \qquad CC_c \neq \emptyset \\
\quad cc^{(j,u)} \in CC_c \qquad \text{wo, } \mathcal{E} \vdash \text{conf}\{CC\} \rightsquigarrow_{CC_j} \text{conf}'\{CC'\} \\
\qquad \hfill \text{wo, } \mathcal{E} \vdash [\text{conf}\{CC\}]_{CC}^{\mathcal{L}, \mathcal{T}} \rightsquigarrow_{\mathcal{G}} [\text{conf}'\{CC'\}]_{CC}^{\mathcal{L}, \mathcal{T}}
\end{array}
$$

$$
\begin{array}{l}
\text{CALLSDONE} \\
\quad CC = \{CC_r, CC_c, CC_t, CC_e\} \qquad CC_c = \emptyset \\
\quad \text{wo, } \mathcal{E} \vdash [\text{conf}\{CC\}]_{CC}^{\mathcal{L}, \mathcal{T}} \rightsquigarrow_{\mathcal{G}} [\text{conf}\{CC\}]_{RN}^{\mathcal{L}, \mathcal{T}}
\end{array}
$$

<caption>Figure 5.40: Semantic rules for Step 6</caption>

In this case, the rule label of the scheduler execution context is set to CC. Note that the last premise is |CC<sub>e</sub>| ≠ |CC|, meaning the cardinality of the partition and the whole set CC differ. There are still clients that might call or have a chunk to run.

If the last premise is |CC<sub>e</sub>| = |CC|, then the last rule applies, namely WebiDone.
The rule label is set to end, meaning that the scheduler must stop executing, and conf becomes the final configuration.

Step 6, CC This scheduling step is concerned with applying, wherever possible, the CLIENTCALL rule. We provide the small-step rules in Figure 5.40. The CallChoosen rule picks a client *j* from the partition set *CC*<sub>*c*</sub>.

The client performs a ClientCall step, returning an updated configuration. The sched-
uler context is updated with the new configuration conf'.

Otherwise, the *CallsDone* applies when the partition set *CC*<sub>*c*</sub> is empty, meaning
there are no more calls to evaluate this iteration. Hence, this rule updates the rule label
to *RN* for going to the next step.

Step 7, RN In the last step of the scheduler, we present rules for handling the Run rule application. Similarly to the device’s rules, the order in which thunks execute matters. For example, consider two thunks of a client, one that wants to call a service that opens the window and one that calls the one that closes it—the observations made on the final L of the final WEBI configuration change depending on the order of the chunk choice. Hence, this step is guided by T, the filtering of the non-deterministic trace describing
Step 7

$$
\begin{array}{l}
\textsc{RunChosen} \\
\mathcal{T} = (j, i) :: \mathcal{T}' \qquad CC = \{CC_r, CC_c, CC_t, CC_e\} \\
\langle cc, B, T \rangle^{(j,u)} \in CC_t \qquad t^i \in T \qquad \mathit{wo}, \mathcal{E} \vdash \mathit{conf}\{CC\} \rightsquigarrow_{\mathbb{RN}_{(j,i)}} \mathit{conf}'\{CC'\} \\
\hline
\mathit{wo}, \mathcal{E} \vdash [\mathit{conf}\{CC\}]_{\mathbb{RN}}^{\mathcal{L}, \mathcal{T}} \rightsquigarrow_{\mathcal{G}} [\mathit{conf}'\{CC'\}]_{\mathbb{RN}}^{\mathcal{L}, \mathcal{T}'}
\end{array}
$$

$$
\begin{array}{l}
\textsc{RunNotFound} \\
\mathcal{T} = (j, i) :: \mathcal{T}' \qquad CC = \{CC_r, CC_c, CC_t, CC_e\} \\
\langle cc, B, T \rangle^{(j,u)} \in CC_t \qquad t^i \notin T
\end{array}
$$

$$
\mathit{wo}, \mathcal{E} \vdash [\mathit{conf}\{CC\}]_{\mathbb{RN}}^{\mathcal{L}, \mathcal{T}} \rightsquigarrow_{\mathcal{G}} [\mathit{conf}\{CC\}]_{\mathbb{SS}}^{\mathcal{L}, \mathcal{T}}
$$

$$
\begin{array}{l}
\textsc{RunDone} \\
CC = \{CC_r, CC_c, CC_t, CC_e\} \\
\mathcal{T} = [] \wedge CC_t = \emptyset \\
\hline
\mathit{wo}, \mathcal{E} \vdash [\mathit{conf}\{CC\}]_{\mathbb{RN}}^{\mathcal{L}, \mathcal{T}} \rightsquigarrow_{\mathcal{G}} [\mathit{conf}\{CC\}]_{\mathbb{SS}}^{\mathcal{L}, \mathcal{T}}
\end{array}
$$

<caption>Figure 5.41: Semantic rules for Step 7</caption>

the order of the RN rule application.

The rule RunChosen applies the RN WEBI transition, executing the chunk (j, i), which is the head of the list T. A constraint is that the chunk i of the client j must exist. The rule returns the new WEBI configuration and updates the scheduler context with the T deprived of its head.

Otherwise, the rule RunNotFound applies if the chunk does not belong to the client's set T. It means that the chunk is still a callback, or the client has not yet called the service (j, i). In this case, the rule label of the scheduler context changes to SS. We keep the order of the RN applications. We remark that step 1 of the scheduler is executed only in the first iteration. Afterward, the scheduler does not consider further client initializations.

Finally, if the list T is empty, no other client's chunk will ever be executed. The scheduler directly passes to the second step.

5.3.2 Equivalence of the Scheduler and the WEBI Semantics

The scheduler semantics we propose must achieve two goals:
* All the traces produced must be correct, by preserving the original behavior of the model.

* Reproduce all the traces that provide observations of sensitive events.

We define Theorem 1 saying that given an initial WEBI configuration setting conf, after a finite number of steps $n$, the model execution will produce a final configuration $conf_n$ only if exists a number of finite steps on conf—$n+k$-that the scheduler can execute producing a final configuration $conf_{(n+k)}$ equivalent to $conf_n$.

Intuitively, every WEBI non-deterministic execution produces the same observations as the ones resulting from a scheduler execution and vice versa.

**Theorem 1 (Scheduler's Equivalence to WEBI)** *Considering the constraints presented by Hypotheses 1, 2, 3, 4, and 5 given a well-formed initial WEBI configuration conf:*

$$ \forall wo, \mathcal{E}, n, \Pi, conf_n, \mathcal{L}, \mathcal{L}', conf_n. $$

$$ \exists k: $$

$$ wo, \mathcal{E} \vdash \mathrm{conf}\{\emptyset, \emptyset\} \rightsquigarrow^n conf_n\{\mathcal{L}, \Pi\} $$

$$ \Leftrightarrow $$

$$ (wo, \mathcal{E} \vdash [[\mathrm{conf}]_{\mathbb{N}}^{(\pi_{\mathcal{L}}(\Pi), \pi_{\mathcal{S}}(\Pi))} \rightsquigarrow^{(n+k)} [[\mathrm{conf}_{(n+k)}]]^{[1], [1]}) \wedge conf_n = conf_{(n+k)} $$

Considering the $\Leftarrow$ direction of the proof, the proof is trivial; the other direction is challenging. Indeed, we must prove that given it exists a transformation of every WEBI trace to an equivalent scheduler trace. It follows that, if the new trace is executed by the WEBI then it is executed also by the scheduler. The transformation of the trace is obtained via trace permutations. Hence, we define two series of lemmas:

* A series of lemmas representing an order relation among WEBI rule transitions—Section 5.3.2.1.

* A series of lemmas for constructing intervals that represent the scheduling steps—Section 5.3.2.2.

### 5.3.2.1 Commutation Lemmas

To achieve the goal of transforming a non-deterministic trace into a scheduler's one, we must define the commutation of consequent WEBI transition relations. We define
Generic form of the lemmas

$\forall \text{conf}, \text{conf}^\prime, \text{conf}^\prime\prime, \mathcal{X}.$

$\text{conf} \rightsquigarrow_{\mathcal{X}} \text{conf}^\prime \rightsquigarrow_{\text{Rule}} \text{conf}^\prime \wedge$

Constraints

$\Rightarrow$

$\exists \text{conf}^\prime\prime\prime.$

$\text{conf} \rightsquigarrow_{\text{Rule}} \text{conf}^\prime\prime\prime \rightsquigarrow_{\mathcal{X}} \text{conf}^\prime$

<table><caption>Figure 5.42: At the top of the figure, we show an informal generic definition of the lemmas. The table shows, for each rule, the rules with which to commute and the constraints of the commutations.</caption><thead><tr><th>Rule</th><th>X</th><th>Constraints</th></tr></thead><tbody><tr><td>IN</td><td>{IN, SS, RS, CS, CC, RN, DV}</td><td>X</td></tr><tr><td>SS<sub>(j,i)</sub></td><td>{SS, RS<sub>(j',i')</sub>, CS, CC, RN, DS, DA<sub>(j',i')</sub>, DR<sub>(j',i')</sub>}</td><td>(j ≠ j' ∨ i ≠ i') ∧ conf{CC} ∧ (∃cc, b<sup>i</sup> ∈ B, T<sup>(j,u)</sup> ∈ CC ∨ &lt;boot&gt;<sup>(j,u)</sup> ∈ CC)</td></tr><tr><td>RS<sub>(j,i)</sub></td><td>{RS<sub>(j',i')</sub>, CS, CC, RN, DS, DA<sub>(j',i')</sub>, DR<sub>(j',i')</sub>}</td><td>(j ≠ j' ∨ i ≠ i') ∧ conf{CC} ∧ (∃cc, b<sup>i</sup> ∈ B, T<sup>(j,u)</sup> ∈ CC ∨ &lt;boot&gt;<sup>(j,u)</sup> ∈ CC)</td></tr><tr><td>DS</td><td>{CC, RN, DS}</td><td>X</td></tr><tr><td>DA<sub>(j,i)</sub><br>DR<sub>(j,i)</sub></td><td>{CS, CC, RN}</td><td>conf{CC} ∧ (∃cc, b<sup>i</sup> ∈ B, T<sup>(j,u)</sup> ∈ CC)</td></tr><tr><td>CS<sub>j</sub></td><td>{CS, CC<sub>j'</sub>, RN<sub>(j',i)</sub>}</td><td>j ≠ j'</td></tr><tr><td>CC<sub>j</sub></td><td>{CC, RN}</td><td>j ≠ j'</td></tr></tbody></table>

a series of lemmas to provide a commutation relation between rule applications. In Table 5.42, we present this series of lemmas, showing on the first column the rule we want to commute, on the second column the set of rules commuting with it, and on the third column constraints if any. We formally present only the commutation lemmas for the ServiceInit, ServiceStep, and the device rules—DeviceSensor, DeviceActuator, and DeviceReading-. All the lemmas that concern the other rules follow the ones we describe.

First, we define the commutation lemma for the IN rule, as it is the rule repeatedly applied in the first execution step of the scheduler (Lemma 1).
**Lemma 1 (Trace commutativity(IN))** A ServiceInit transition relation can commute with all the other transitions. Commuting transitions results in the same final configuration.

$$ 
\begin{array}{l}
\forall \text{conf}, \text{conf}', \text{conf}'', X : \\
X \in \{\text{IN}, \text{SS}, \text{RS}, \text{CS}, \text{CC}, \text{RN}, \text{DV}\} \wedge wo, \mathcal{E} \vdash \text{conf} \rightsquigarrow_X \text{conf}'' \rightsquigarrow_{\text{IN}} \text{conf}' \\
\Rightarrow \\
\exists \text{conf}''' : wo, \mathcal{E} \vdash \text{conf} \rightsquigarrow_{\text{IN}} \text{conf}''' \rightsquigarrow_X \text{conf}'
\end{array}
$$

We proved this lemma by case analysis on $X$, showing that commuting the transition relation does not change the terminal configuration $conf'$. We show that, for each case we can commute the transition relation obtaining the same final configuration. Hence, repeatedly applying this lemma to a trace, batches all ServiceInits present in the trace in the beginning. The transformation does not change the overall meaning of the trace. Indeed, the final configuration produced by executing WEBI following the reordered trace is equivalent to the original.

Similarly, we define a lemma for commuting the ServiceStep transition relation with a subset of $X$. We present this commutation property in Lemma 2.

**Lemma 2 (Trace commutativity(SS))** Given $conf$, a WEBI configuration, and assuming limitations on the model described in the Hypotheses 1, 3, and 4:

$$ 
\begin{array}{l}
\forall \text{conf}, \text{conf}', \text{conf}'', X, j, i, cc^{(j,u)}, b^i, CC \\
X \in \{\text{SS}, \text{RS}_{(j',i')}, \text{CS}, \text{CC}, \text{RN}, \text{DS}, \text{DA}_{(j',i')}, \text{DR}_{(j',i')}\} \wedge (j \neq j' \lor i \neq i') \wedge \\
\text{conf}\{\text{CC}\} \wedge ((cc, b^i \in B, T\rangle^{(j,u)} \lor \langle\text{boot}\rangle^{(j,u)} \in \text{CC}) \wedge \\
wo, \mathcal{E} \vdash \text{conf}'' \rightsquigarrow_X \text{conf}'' \rightsquigarrow_{\text{SS}(j,i)} \text{conf}' \\
\Rightarrow \\
\exists \text{conf}''' : wo, \mathcal{E} \vdash \text{conf} \rightsquigarrow_{\text{SS}(j,i)} \text{conf}''' \rightsquigarrow_X \text{conf}'
\end{array}
$$

The lemma's proof is similar to the Lemma 1, obtaining the same result. There are three particular cases we want to discuss: commutation with another $SS_{(j',i')}$—where $j \neq j' \land i \neq i'$, with an $RS_{(j,i)}$, and with the device rules. Regarding the commutation with another service, we know it is possible commute with the $SS_{(j,i)}$ service, even if running on the same host. This is allowed because of the hypotheses regarding the
determinism of the server language and the untouched host memory. The $RS_{(j,i)}$ never commutes with a future service step on the service $(j, i)$. The reason is that the service $(j, i)$ returns a value to the client. Afterward, it cannot step anymore. Hence, does not exist a trace that has a segment produced by the following sequence of transition relations: $wo, \mathcal{E} \vdash \text{conf}'' \rightsquigarrow_{RS_{(j,i)}} \text{conf}'' \rightsquigarrow_{SS_{(j,i)}} \text{conf}'$. Regarding devices, the service step can commute only with the device sensor transition, and the device actuator or reading signed by $j \neq j' \land i \neq i'$. Allowing commutation with an actuator or reading application of the same service means concretely to swap the service's lines of code.

Finally, we present three lemmas, one for each device rule—DS (Lemma 3), DA (Lemma 4), and DR (Lemma 5).

**Lemma 3 (Trace commutativity(DS))** *Given* conf, a WEBI configuration:

$$ \forall X, \text{conf}, \text{conf}', \text{conf}'' $$

$$ X \in \{DS, CS, CC, RN\} \wedge wo, \mathcal{E} \vdash \text{conf} \rightsquigarrow_X \text{conf}'' \rightsquigarrow_{DS} \text{conf}' $$

⇒

$$ \exists \text{conf}''' : wo, \mathcal{E} \vdash \text{conf} \rightsquigarrow_{DS} \text{conf}''' \rightsquigarrow_X \text{conf}' $$

**Lemma 4 (Trace commutativity(DA))** *Given* conf, a webi configuration

$$ \forall X, \text{conf}, \text{conf}', \text{conf}'' $$

$$ X \in \{CS, CC, RN\} \wedge \text{conf}\{CC\} \wedge \langle cc, b^i \in B, T \rangle^{(j,u)} \in CC \wedge wo, \mathcal{E} \vdash \text{conf} \rightsquigarrow_X \text{conf}'' \rightsquigarrow_{DA_{(j,i)}} \text{conf}' $$

⇒

$$ \exists \text{conf}''' : wo, \mathcal{E} \vdash \text{conf} \rightsquigarrow_{DA_{(j,i)}} \text{conf}''' \rightsquigarrow_X \text{conf}' $$

**Lemma 5 (Trace commutativity(DR))** *Given* conf, a webi configuration:

$$ \forall X, \text{conf}, \text{conf}', \text{conf}'' $$

$$ X \in \{CS, CC, RN\} \wedge \text{conf}\{CC\} \wedge \langle cc, b^i \in B, T \rangle^{(j,u)} \in CC \wedge wo, \mathcal{E} \vdash \text{conf} \rightsquigarrow_X \text{conf}'' \rightsquigarrow_{DR_{(j,i)}} \text{conf}' $$

⇒

$$ \exists \text{conf}''' : wo, \mathcal{E} \vdash \text{conf} \rightsquigarrow_{DR_{(j,i)}} \text{conf}''' \rightsquigarrow_X \text{conf}' $$
Also for these three lemmas, the proof approach is similar to the IN and SS lemmas. Regarding the device sensor lemma, we allow commutation among DSs, but not with DA and DR. For an actuation or a reading, putting a DS before or after changes the meaning of the world record $\mathcal{L}$. For example, allowing a commutation with a $DR_{(j,i)}$ would probably mean reading a different value from the device memory, as the DeviceSensor rule produces a physical event and updates some devices' memories. For Lemma 4 and Lemma 5, we permit commutations only with the following client-driven rules: CS, CC, and RN.

### 5.3.2.2 Interval Lemmas

The lemmas presented in Section 5.3.2.1 can be seen as the definition of order relations between WEBI labeled transitions $wo, \mathcal{E} \vdash (\rightsquigarrow_X R \rightsquigarrow_{X'})$, for some $X, X'$, $wo, \mathcal{E}$, and an order relation $R$. These relations are fundamental for reordering the non-deterministic trace, obtaining an equivalent reordered one. The intuition behind the design of these lemmas is to reorder the trace using a sorting-like algorithmic approach.

In this section, we show two lemmas, one for creating an interval of ServiceInits (step 1), and one for creating an interval of device rule applications (step 4). The other lemmas—one for each scheduler step-follow the two we define in the section.

Concerning step 1, we present the proposition in Lemma 6. To provide some notation, $\Pi_1 :: \Pi_2$ represents the concatenation of two traces, $\rightsquigarrow^n$ denotes multiple WEBI execution steps, $\rightsquigarrow^k \Pi$ denotes $k$ WEBI execution steps guided by the trace $\Pi$, and $|\Pi|$ represents the length of a trace.

We say that we can reorder a finite final trace $\Pi_n$, obtaining two traces, $\Pi^IN$ and $\Pi^{-IN}$, respectively, the trace of the IN rules application and the rest of the trace. A WEBI execution guided by the trace $\Pi^IN :: \Pi^{-IN}$ results in a final configuration equal to the one produced by executing the trace $\Pi^IN :: \Pi^{-IN}$.

**Lemma 6 (IN Interval)** *Given a well-formed initial WEBI configuration conf and a final*
configuration $conf_n$ produced after $n$ steps of executing WEBI:

$$ \forall wo, \mathcal{E}, \text{conf}, \mathcal{I}, HM, IC, n, \text{conf}_n, CC_e \mathcal{L}, IC', \Pi. $$

$$ \mathcal{I} \neq \emptyset \quad \wedge \quad \text{conf} = \langle \emptyset, \mathcal{I}, HM, \{\emptyset, \emptyset, \emptyset, \emptyset\}, \{\emptyset, \emptyset, \emptyset, \emptyset\}, IC, \emptyset \rangle $$

$$ \wedge wo, \mathcal{E} \vdash \text{conf} \rightsquigarrow^n \text{conf}_n \wedge $$

$$ \text{conf}_n = \langle \mathcal{L}, \emptyset, HM, \{\emptyset, \emptyset, \emptyset, \emptyset\}, \{\emptyset, \emptyset, \emptyset, CC_e\}, IC', \Pi \rangle \wedge |\mathcal{I}| = |CC_e| $$

$$ \Rightarrow $$

$$ \exists \text{conf}_{k1}, \text{conf}'_n, k1, k2, \Pi^{\text{IN}}, \Pi^{-\text{IN}}. $$

$$ |\Pi^{\text{IN}}| + |\Pi^{-\text{IN}}| = k1 + k2 = n = |\Pi| \quad \wedge \quad |\Pi^{-\text{IN}}| < |\Pi| \quad \wedge $$

$$ \text{conf}_{k1} = \langle \emptyset, \emptyset, HM, \{SS_r, \emptyset, \emptyset, \emptyset\}, \{CC_r, \emptyset, \emptyset, \emptyset\}, IC, \Pi^{\text{IN}} \rangle $$

$$ \wedge SS_r \neq \emptyset \quad \wedge \quad CC_r \neq \emptyset \quad \wedge \quad wo, \mathcal{E} \vdash \text{conf} \rightsquigarrow_{\Pi^{\text{IN}}}^{k1} \text{conf}_{k1} \rightsquigarrow_{\Pi^{-\text{IN}}}^{k2} \text{conf}'_n \wedge $$

$$ \text{conf}'_n = \langle \mathcal{L}, \emptyset, HM, \{\emptyset, \emptyset, \emptyset, \emptyset\}, \{\emptyset, \emptyset, \emptyset, CC_e\}, IC', \Pi^{\text{IN}} \:: \Pi^{-\text{IN}} \rangle $$

We proved Lemma 6 by strong induction on the length of the trace. We repeatedly apply Lemma 1 to every proof sub-case. Note that we deal with finite traces. Hence, we need a notion of reduction. On the right-hand side of the arrow, the condition $|\Pi^{-\text{IN}}| < |\Pi|$ is satisfied, as reordering a portion of the trace makes the unordered part smaller than the original $\Pi$.

Regarding devices, we present the interval reordering in Lemma 7. We say that there always exists a reordering $\Pi^{\text{DV}} :: \Pi^{-\mathcal{G}}$ of a non-ordered sub-trace $\Pi^{-\mathcal{G}}$ such that an execution of a trace $\Pi^{\text{IN}} :: \Pi^{\mathcal{G}} :: \Pi^{-\mathcal{G}}$ results in a final WEBI configuration equivalent to the one produced by executing $\Pi^{\text{IN}} :: \Pi^{\mathcal{G}} :: \Pi^{\text{DV}} :: \Pi^{-\mathcal{G}}$.

The portion $\Pi^{\text{DV}}$ of the trace is an interval of device rules.

**Lemma 7 (DV Interval)** Given $conf$, an initial well-formed WEBI configuration, a finite portion of a trace $\Pi, \Pi^{\text{IN}} :: \Pi^{\mathcal{G}}$, where $\Pi^{\text{IN}}$ represents the step 1 reordering and $\Pi^{\mathcal{G}}$
some other reordering steps, $\Pi^{-\mathfrak{G}}$ a finite non-reordered part of the trace:

$$ \forall wo, \mathcal{E}, k1, k2, n, \text{conf}, \text{conf}_{k1}, \text{conf}_n, \mathcal{I}, HM, SS_a, SS_g, $$

$$ CC_r, CC_e, CC'_e, IC, IC', IC'', \mathcal{L}, \mathcal{L}', \Pi^{\mathbb{IN}}, \Pi^{\mathfrak{G}}, \Pi^{-\mathfrak{G}}. $$

$$ |\Pi^{\mathbb{IN}}| + |\Pi^{\mathfrak{G}}| = k1 \quad \wedge \quad k1 + |\Pi^{-\mathfrak{G}}| = n \quad \wedge $$

$$ \text{conf} = \langle \emptyset, \mathcal{I}, HM, \{\emptyset, \emptyset, \emptyset, \emptyset\}, \{\emptyset, \emptyset, \emptyset, \emptyset\}, IC, \emptyset \rangle \quad \wedge $$

$$ wo, \mathcal{E} \vdash \text{conf} \rightsquigarrow_{(\Pi^{\mathbb{IN}}::\Pi^{\mathfrak{G}})}^{k1} \text{conf}_{k1} \rightsquigarrow_{\Pi^{-\mathfrak{G}}}^{k2} \text{conf}_n \quad \wedge $$

$$ \text{conf}_{k1} = \langle \mathcal{L}', \emptyset, HM, \{\emptyset, SS_a, SS_g, \emptyset\}, \{CC_r, \emptyset, \emptyset, CC'_e\}, IC'', \Pi^{\mathbb{IN}} :: \Pi^{\mathfrak{G}} \rangle $$

$$ \wedge \quad \text{conf}_n = \langle \mathcal{L}, \emptyset, HM, \{\emptyset, \emptyset, \emptyset, \emptyset\}, \{\emptyset, \emptyset, \emptyset, \emptyset\}, IC', \Pi^{\mathbb{IN}} :: \Pi^{\mathfrak{G}} :: \Pi^{-\mathfrak{G}} \rangle $$

$$ \wedge \quad |\mathcal{I}| = |CC_e| \quad \wedge \quad |CC'_e| < |\mathcal{I}| $$

$\Rightarrow$

$$ \exists k1', k2', \text{conf}_{(k1+k1')}, \text{conf}'_n, SS_r, SS'_a, SS'_g, IC''', \mathcal{L}'', \Pi^{(\mathbb{DV})}, \Pi^{-\mathfrak{G}'} $$

$$ |\Pi^{-\mathfrak{G}}| = k2 = k1' + k2' = |\Pi^{(\mathbb{DV})}| + |\Pi^{-\mathfrak{G}'}| \quad \wedge \quad |\Pi^{-\mathfrak{G}'}| \leq |\Pi^{-\mathfrak{G}}| \quad \wedge $$

$$ wo, \mathcal{E} \vdash \text{conf} \rightsquigarrow_{(\Pi^{\mathbb{IN}}::\Pi^{\mathfrak{G}})}^{k1} \text{conf}_{k1} \rightsquigarrow_{\Pi^{(\mathbb{DV})}}^{k1'} \text{conf}_{(k1+k1')} \rightsquigarrow_{\Pi^{-\mathfrak{G}'}}^{k2'} \text{conf}'_n \quad \wedge $$

$$ \text{conf}_{(k1+k1')} = \langle \mathcal{L}'', \emptyset, HM, \{SS_r, SS'_a, SS'_g, \emptyset\}, \{CC_r, \emptyset, \emptyset, CC'_e\}, IC''', \Pi^{\mathbb{IN}} :: \Pi^{\mathfrak{G}} :: \Pi^{(\mathbb{DV})} \rangle \wedge $$

$$ \text{conf}'_n = \langle \mathcal{L}, \emptyset, HM, \{\emptyset, \emptyset, \emptyset, \emptyset\}, \{\emptyset, \emptyset, \emptyset, \emptyset\}, IC', \Pi^{\mathbb{IN}} :: \Pi^{\mathfrak{G}} :: \Pi^{(\mathbb{DV})} :: \Pi^{-\mathfrak{G}'} \rangle $$

We use Lemmas 3, 4, and 5 to prove this lemma for applying commutations on the non-ordered trace $\Pi^{-\mathfrak{G}}$, resulting in a trace with a segment of $\mathbb{DV}$ rules (step 4), equivalent to the original—producing the same final WEBI configuration. We proceed by strong induction on the trace $\Pi^{-\mathfrak{G}}$. We can always create an interval of $\mathbb{DV}$s when $SS_g$ or $SS_a$ is not empty. Note that this interval could be empty if no device commutation lemma applies. In this case, the trace segment $\Pi^{-\mathfrak{G}}$ does not reduce. The postcondition $|\Pi^{-\mathfrak{G}'}| \leq |\Pi^{-\mathfrak{G}}|$ reflects this case.

### 5.3.2.3 Proof Sketch of Theorem 1

- $\Leftarrow$ This direction is trivial. The non-deterministic WEBI semantics can always imitate a scheduler's step. Indeed, if the scheduler semantics can step, it is possible to do a step with non-deterministic WEBI.

- $\Rightarrow$ We divide the proof into two steps. The first step reorders a non-deterministic trace by applying the commutation lemmas presented in Section 5.3.2.2 to create
ate a sequence of intervals in the trace. We show that the trace $Π_n$ and the re-
arranged (partially-ordered) trace $Π'_n$ produce equivalent executions. We prove
this step by defining two trace reordering iterations: one for the first iteration of the
scheduler, comprehending the ServiceInits, and the other for the successive it-
erations, which do not consider the scheduler's first step. For each sub-case, the
final configuration is equivalent to the one obtained by executing the WEBI on the
original one. Hence, the trace transformation is correct for the non-deterministic
WEBI semantics. The proof comes almost in an algorithmic fashion. Despite its
size, this proof step comes straightforward, as we rely on the commutation and
the interval lemmas. The initial hypotheses we consider are the following.

$wo, \mathcal{E} \vdash \mathrm{conf} \rightsquigarrow^n \mathrm{conf}_n$

$$
\mathrm{conf} = \langle \emptyset, \mathcal{I}, \mathrm{HM}, \{\emptyset, \emptyset, \emptyset, \emptyset\}, \{\emptyset, \emptyset, \emptyset, \emptyset\}, \mathrm{IC}, \emptyset \rangle
$$

$$
\mathrm{conf}_n = \langle \mathcal{L}, \emptyset, \mathrm{HM}, \{\emptyset, \emptyset, \emptyset, \emptyset\}, \{\emptyset, \emptyset, \emptyset, \mathrm{CC}_e\}, \mathrm{IC}', \Pi_n \rangle
$$

Moreover, the hypotheses we consider are the one listed in Section 5.3.1.1.

For the second step, we consider an ordered trace equivalent to Πₙ, called Π'ₙ =
Π<sup>IN</sup> :: Π<sup>S</sup>. Knowing that they produce equivalent executions, we show that both
the scheduler and WEBI can simulate the ordered trace. We rewrite the theorem
in the following proposition.

$$
\forall wo, \mathcal{E}, n, \Pi^{\mathbb{N}} :: \Pi^{\mathcal{S}}, \mathrm{conf}_n, \mathrm{conf}'_n. \exists t :
$$

$$
wo, \mathcal{E} \vdash \mathrm{conf}(\emptyset) \rightsquigarrow^n \mathrm{conf}_n\{\Pi^{\mathbb{N}} :: \Pi^{\mathcal{S}}\}
$$

->

$$
(wo, \mathcal{E} \vdash [\mathrm{conf}]_{\mathrm{IN}}^{\pi_{\mathcal{S}}(\Pi^{\mathrm{IN}}::\Pi^{\mathcal{S}}), \pi_{\mathcal{S}}(\Pi^{\mathrm{IN}}::\Pi^{\mathcal{S}})} \rightsquigarrow^{(n+t)} [\mathrm{conf}'_{(n)}]_{\mathrm{end}}^{[1,1]} \wedge \mathrm{conf}'_n = \mathrm{conf}_n
$$

For simplicity, we rename Π<sup>IN</sup> :: Π<sup>S</sup> as Π'<sup>S</sup>, where |Π'<sup>S</sup>| = n. If the trace size n is 0, the proof is trivial. Otherwise, we define an induction predicate stating that the scheduler can always imitate the reordered trace for some generic k + t steps, where t is the number of scheduler transitions that do not change the
configuration. We show the induction predicate in the following proposition:

$$ \forall n, k, \Pi^{\mathcal{G}}, \Pi^{\mathbb{N}} :: \Pi^{\mathcal{G}}, \text{conf}, \text{conf}_k. $$

$$ \begin{align*} \Pi^{\mathbb{N}} &:: \Pi^{\mathcal{G}} = \Pi^{\mathcal{G}} \wedge |\Pi^{\mathcal{G}}| = n \wedge \text{conf} &\leadsto_{\Pi^{\mathcal{G}}_{[0,k]}}^{k} \text{conf}_k \\ &\Rightarrow \\ &\exists t, \mathcal{X}. \end{align*} $$

$$ \begin{gather*} [[\text{conf}]]_{\mathbb{N}}^{\pi_{\mathcal{L}}(\Pi^{\mathcal{G}}), \pi_{\mathcal{F}}(\Pi^{\mathcal{G}})} \leadsto_{\mathcal{G}}^{(k+t)} [[\text{conf}'_k]]_{\mathcal{X}}^{\pi_{\mathcal{L}}(\Pi^{\mathcal{G}}_{[k+1,n]}), \pi_{\mathcal{F}}(\Pi^{\mathcal{G}}_{[k+1,n]})} \wedge \\ \text{conf}'_k = \text{conf}_k \end{gather*} $$

, where $\Pi^{\mathcal{G}}_{[0,k]}$ is the subtrace of $\Pi^{\mathcal{G}}$ from the index 0 to $k$.

We assume that this predicate hold for $k$ steps. We show that it also holds for every next step $k+1$. We go by case analysis on $k$, showing that the scheduler and the non-deterministic semantics can do $k+t$ and $k$ steps respectively, following the trace $\Pi^{\mathcal{G}}_{[0,k]}$.

Then, for each possible sub-case, we show that both the semantics can perform one more execution step to produce the same $k+1$ configuration.

The induction predicate holds for every subcase; hence we conclude the proof by saying that the scheduler's execution can produce every final configuration generated by a WEBI execution, making the semantics equivalent.

### 5.3.3 Executing the Example of Section 5.2.3 in Skel

In the section, we show how the implementation of the scheduler in Skel is suitable for executing the example presented in Section 5.2.3.

**Skel Implementation.** The scheduler semantics we proposed is one designed for proving the equivalence theorem. To implement the scheduler, we could have implemented it by providing as input $\mathcal{L}$ and $\mathcal{T}$. However, the usability of the scheduler would then be complex. Thus, we relax the input that should be provided and implement a scheduler such that:

* Scheduling step 4 does not follow the trace $\mathcal{L}$.
* Scheduling step 7 does not follow the trace $\tau$.

To observe the possible interaction in the scheduler's execution, we design steps 4 and 7 to be non-deterministic, similarly to diagram B in Figure 5.33. Indeed, we exploit the Skel branch construct for deciding whether to pick and execute configurations with elements from $SS_a$, $SS_g$, or $CC_t$, or not.

All the other steps are immuted, emptying the related partition set before passing to the next scheduling step.

We derive two interpreters from the Skel definition, one using the RandID interpretation monad and the other using the List monad. One can find the examples in the following repository: https://gitlab.inria.fr/skeletons/webi-in-skel/-/tree/master.

**Two Scheduler Executions.** We showed that reducing the non-determinism of the model does not affect the expressiveness of WEBI. The OCaml interpreter generated from the scheduler's semantics produces all the possible traces generated by the original semantics interpreter's executions. This section presents two traces equivalent to traces A and B described in Figure 5.32. The result of executing these traces produces final WEBI configurations congruent to the ones presented in Section 5.2.3. We remark that the interpreter follows the behavior of the diagram shown in Figure 5.33.

Figure 5.43 presents the equivalent traces resulting from a concrete interpretation. These two traces perform four scheduler iterations.

The first iteration starts on both cases with two `ServiceInits`, and the order of the initializations is not essential. Afterward, both the services perform `ServiceSteps`, choosing to do two steps on a row on the `windowManager` and one on the `tunOnOven` service. The resulting configuration contains the oven actuation and the thermometer reading in the partition sets `_SS_a` and `_SS_g`. These devices' interactions belong to the execution of the `windowManager` and the `tunOnOven` running services. The first iteration ends with the device rules applications. Trace A first executes the device actuator of the oven after a device sensor, meaning that the following `DeviceSensor` will update the thermometer memory to 26°, making the `DeviceReading` reading a temperature higher than 24°C. Differently, trace B first executes the `DeviceSensor` and the `DeviceReading`, making the read temperature being a value lower than 24°C.

The second iteration is substantially different between traces A and B. Trace A first makes the window and the oven service code progress via `ServiceSteps`. This
Scheduler's execution equivalent to rule sequence A.

**1st Iteration.**

<figure><img src="image_29.png" /></figure>

**2nd Iteration.**

<figure><img src="image_30.png" /></figure>

**3rd Iteration.**

<figure><img src="image_31.png" /></figure>

**4th Iteration.**

<figure><img src="image_32.png" /></figure>

Scheduler's execution equivalent to rule sequence B.

**1st Iteration.**

<figure><img src="image_33.png" /></figure>

**2nd Iteration.**

<figure><img src="image_34.png" /></figure>

**3rd Iteration.**

<figure><img src="image_35.png" /></figure>

**4th Iteration.**

<figure><img src="image_36.png" /></figure>

Figure 5.43: Two scheduler's reordered traces behaviorally equivalent to the traces in Figure 5.32. With equivalent we mean that they produce the same final WEBI configuration. We annotate the some rules applications with “o” and “w” to refer to the oven and window service, and “a” and “s” to refer to the clients adam and steve.

series of ServiceSteps concludes the oven service evaluation in trace A. Indeed, in the next step, a RetServiceBoot happens, creating a running client. Afterward, a device actuator happens for the windowManager service, and finally, the client is created by the oven service steps, concluding the second iteration. For trace B, things work differently.
Only the `windowManager` steps because the oven actuation is still pending. Afterward, a series of device rules happen by performing an actuation—and closing it-and turning on the oven after a device sensor application. Trace B does not produce a configuration with a detectable interaction between the two devices.

The two traces also differ in the third iteration. Trace A performs some service steps on the `windowManager` service before reaching the thermometer `get`. Afterward, the trace records a device sensor followed by the reading of the only service executing. Trace B completes the execution of the `turnOnOven` service and continues the one of the `windowManager`—similarly to trace A. It follows that the window service reads the thermometer temperature, and finally oven's service returns, creating a running client, ending this iteration.

The fourth iteration of the scheduler is identical for both traces, concluding the execution of the window service, which by returning creates a running client, which with a client step ends its execution too.

### Collecting Semantics.
Execution traces A and B produce the only two final configurations the model can derive. We executed the same program with the collecting semantics monad, obtaining different permutations of the traces, meaning that device rule applications are located differently in the resulting $\mathcal{L}$. Nevertheless, the two final configurations are always equivalent to the ones produced by executing the traces in Figure 5.43.
Conclusion
In this thesis, we defined a practical approach to represent the semantics of pro-
gramming languages via Skel [41], a specification language that concretizes Skeletal
Semantics [8]. In Chapter 3, we have shown how this simple, purely functional meta-
language can easily capture complex target language features by leveraging monadic
operators. We claim the descriptions written in Skel are easy to read and maintain.
Indeed, new meta features (such as the need to manipulate continuations) are seldom
introduced, and when they are, only the monadic binders need to be adapted; existing
descriptions not relying on the feature may be left unchanged.

In addition, existing tools such as *necroml* [42] let us derive an OCaml interpreter from a Skeletal Semantics. We have used it to obtain executable versions of the toy languages presented in this chapter—the arithmetic language and its extension with exceptions, the PCF, the stateful PCF, and the yield language.<fnref n="5" />

In Chapter 4, we have described how can the Skel language be used to mechanize
complex semantics. In particular, we have shown how carefully chosen monads can
help to have a formal description close to the specification while still describing the
complex behaviors of ES. This work applied on a larger scale the technique presented
in Chapter 3. We decided to formalize JavaScript because of two main reasons. First,
we have previous experience dealing with the ES specification [6]. Second, the ES
specification is both very precise and very complex. Hence we do not have to guess
the behavior of the language while making sure Skel can scale. In addition to imple-
menting parts of ES in Skel, we also provide boilerplate code to integrate with existing
JS parsers and implement all the unspecified terms in OCaml. Using necroml, we gen-
erate an OCaml executable semantics.

Our main effort stood in mechanizing the foundations of the language, of which `GetValue` is a good example. We can now easily extend our formalization by following the same systematic approach for other abstract algorithms and language constructs.

We have also evaluated the maintainability of the approach. This project began with the formalization of ECMAScript 2020, but after a few months, we switched to the newer ECMAScript 2021. This process took only a few days of work. Naturally, this will change once we complete the formalization of the standard. Nevertheless, we can produce a list of differences between specifications (as a textual diff), making the amount of work proportional to the extent of changes and not to the specification's size. In particular, unlike other work [6], we only have one mechanization to change instead of many. The

<footnote n="5">5. https://gitlab.inria.fr/akhayam/programming_skel</footnote>
standard changes quite often, not only by modifying algorithmic steps but also by intro-
ducing side-effects into the specification.

The work of this chapter is a real-world language application of the work of Chapter 3). We showed that it is possible to systematically introduce side-effects into a formalization by delegating all the necessary machinery to handle them to some carefully designed monads. It is a well-known result [72], but it is unclear how it could be applied in the context of Skel. The monadic approach lets us introduce a new behavior throughout the specification by simply changing the monad we use. Indeed, a short-term goal is to implement a new monad for manipulating delimited continuations and combining it with the ones presented in this paper. As discussed in Section 4.1.6, we will then be able to implement generators whose execution can be suspended (using *yield*) and resumed. This feature is necessary to implement function calls as its algorithmic description uses a generator. Once function calls are implemented, we can directly run the ECMA-262 test suite.

In the long run, we plan several developments for this work. The first goal is to validate that we can use our mechanized semantics to prove some properties of the language. One property of interest is the guarantee that assertions in the specification are always satisfied. To this end, we will use the *necrocoq* tool [50]. As the formalization of JS helped us refine the Skel language, we believe the generation of a Coq semantics will provide many opportunities to suggest improvements for *necrocoq*. Another goal is to exploit our systematic approach to produce a Skeletal Semantics directly from the ES document, using a tool similar to the one presented by J. Park et al. [59]. Finally, we plan to apply our expertise to formalize other complex languages in Skel. An example could be Python, for which formal semantics has been described on paper [45].

In Chapter 5, we studied Skel from another perspective. We wanted to see if the
language is suitable for designing a non-deterministic model. The model describes the
behavior of distributed systems, which consider connected devices, for writing IoT ap-
plications. Hence, after explaining WEBI extensively, we provided a refined small-step
operational semantics of this pre-existing model and its Skel implementation.
From this implementation, we derived two interpreters on which we showed and ex-
ecuted examples of programs. The first instantiation of the interpreter evaluates pro-
grams returning a result, and the second instantiation collects all the possible execution
traces. However, the collecting interpretation was not executable, as the traces to col-
lect on the naive implementation of WEBI are infinite, making the interpretation run out
of memory.

For this reason, we tamed the non-determinism intrinsic in this model by designing
a scheduled semantics of WEBI equivalent to the original under certain assumptions.
We showed that from a non-deterministic trace, there is always a trace transformation
to build an equivalent scheduler trace for each execution trace. This equivalence re-
sult is vital for enabling preliminary studies on this model. Indeed, at the end of the
chapter, we showed that we executed both the concrete and the collecting semantics
interpreter with the scheduler semantics without having any memory issues. Especially
the collecting semantics is interesting, as it paves the way for analysis of the execu-
tion of programs on WEBI. It is a significant result, as the model, passing its embryonal
phase, is ready for further formal studies, both in program analysis and programming
language semantics. Indeed, a plan for the future is to use a server and a client variant
of the ECMAScript semantics proposed in Chapter 4 to provide formal semantics to a
multi-tier language, such as Hop.js [65]. Thus, we would be able to derive a certified
version of the language, which relies on the certifications of the clients and the service
languages, and write and analyze IoT applications that we will define as secure con-
cerning some security properties. The path is long, but this thesis provides modular
work that can be merged for formally reasoning on IoT applications. As said, the two
directions are to design scalable static analysis techniques on the Skel version of WEBI
and to complete the ECMAScript formalizations for developing a multi-tier language we
will use for writing programs. We will rely on the correctness of the work of Chapter 4
once it is finished.

Final Considerations. The approach presented in Chapter 3 and the semantics of JavaScript described in Chapter 4 pushed the Skel language to evolve. The Skel evolution and the works presented in the thesis went in parallel, showing how a more applicative version of a theoretical framework can lead to the growth of a language that was more of an academic tool for representing toy languages. This consideration is positive, as the goal was to have a language and a set of tools reflecting a theoretical framework usable by programming language designers and programmers. We did not change the essence of the original Skeletal Semantics framework [8], edulcorating it for being intuitive to use for real language formalizations. We claim that our technique leads to building solid formalizations. Moreover, at the time of the writing, we have stable tools for deriving a concrete interpretation [42].
However, the *necrocoq* tool is not yet ready. Once *necrocoq* is complete, Skel will be a powerful tool for encoding and certifying programming language semantics.

The original paper states a result of consistency regarding different interpretations, namely the concrete and the abstract interpretation. Skel's tool environment is evolving to include derivations of annotated artefacts for performing abstract interpretation, making the development of such tool essential to transform Skel into a complete language for semanticists.

Finally, the work done for *WEBI* is introductory. Still, we have all the intents to use the Skel tools to study this model for studying IoT security properties, an actual research problem, as these devices are increasingly part of our everyday life. The aim is to be able to explore IoT application's security via instantiations of the Skel semantics of *WEBI*.

I am confident that Skeletal Semantics and Skel are the perfect cost-effective formal framework and specification language for reaching these goals.
<figure><img src="image_37.png" /></figure>
BIBLIOGRAPHY

[1] Guillaume Ambal, Sergueï Lenglet, and Alan Schmitt, "Certified Abstract Machines for Skeletal Semantics", in: *Certified Programs and Proofs*, Philadelphia, United States, Jan. 2022.

[2] *APACHE Groovy, A multi-faceted language for the Java platform*, URL: https://groovy-lang.org.

[3] J. W. Backus, F. L. Bauer, J. Green, C. Katz, J. McCarthy, A. J. Perlis, H. Rutishauser, K. Samelson, B. Vauquois, J. H. Wegstein, A. van Wijngaarden, M. Woodger, and P. Naur, "Revised Report on the Algorithm Language ALGOL 60", in: *Commun. ACM* **6.1** (1963), pp. 1-17, ISSN: 0001-0782, DOI: 10.1145/366193.366201, URL: https://doi.org/10.1145/366193.366201.

[4] Sandrine Blazy, Zaynah Dargaye, and Xavier Leroy, "Formal Verification of a C Compiler Front-End", in: *FM 2006: Int. Symp. on Formal Methods*, vol. 4085, Lecture Notes in Computer Science, Springer, 2006, pp. 460-475, URL: http://xavierleroy.org/publi/cfront.pdf.

[5] Sandrine Blazy and Xavier Leroy, "Formal verification of a memory model for C-like imperative languages", in: *International Conference on Formal Engineering Methods (ICFEM 2005)*, vol. 3785, Lecture Notes in Computer Science, Springer, 2005, pp. 280-299, URL: http://xavierleroy.org/publi/memory-model.pdf.

[6] Martin Bodin, Arthur Charguéraud, Daniele Filaretti, Philippa Gardner, Sergio Maffeis, Daiva Naudziuniene, Alan Schmitt, and Gareth Smith, "A Trusted Mechanised JavaScript Specification", in: *Conference Record of the Annual ACM Symposium on Principles of Programming Languages* 49 (Jan. 2014), pp. 87-100, DOI: 10.1145/2578855.2535876.

[7] Martin Bodin, Arthur Charguéraud, Daniele Filaretti, Philippa Gardner, Sergio Maffeis, Daiva Naudziuniene, Alan Schmitt, and Gareth Smith, *JSCert: Certified JavaScript*, URL: https://jscert.org.
[8] Martin Bodin, Philippa Gardner, Thomas Jensen, and Alan Schmitt, "Skeletal Semantics and their Interpretations", in: *Proceedings of the ACM on Programming Languages* 44 (2019), pp. 1-31, DOI: 10.1145/3290357, URL: https://hal.inria.fr/hal-01881863.

[9] Martin Bodin, Thomas Jensen, and Alan Schmitt, "Certified Abstract Interpretation with Pretty-Big-Step Semantics", in: *Proceedings of the 2015 Conference on Certified Programs and Proofs*, CPP '15, Mumbai, India: Association for Computing Machinery, 2015, pp. 29-40, ISBN: 9781450332965, DOI: 10.1145/2676724.2693174, URL: https://doi.org/10.1145/2676724.2693174.

[10] Denis Bogdanas and Grigore Roşu, "K-Java: A Complete Semantics of Java", in: *Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages*, POPL '15, Mumbai, India: Association for Computing Machinery, 2015, pp. 445-456, ISBN: 9781450333009, DOI: 10.1145/2676726.2676982, URL: https://doi.org/10.1145/2676726.2676982.

[11] Gérard Boudol, Zhengqin Luo, Tamara Rezk, and Manuel Serrano, "Reasoning about Web Applications: An Operational Semantics for HOP", in: *ACM Trans. Program. Lang. Syst.* 34.2 (June 2012), ISSN: 0164-0925, DOI: 10.1145/2220365.2220369, URL: https://doi.org/10.1145/2220365.2220369.

[12] *CAKEML: A Verified Implementation of ML*, URL: https://cakeml.org.

[13] Z. Berkay Celik, Leonardo Babun, Amit K. Sikder, Hidayet Aksu, Gang Tan, Patrick McDaniel, and A. Selcuk Uluagac, "Sensitive Information Tracking in Commodity IoT", in: *Proceedings of the 27th USENIX Conference on Security Symposium*, SEC '18, Baltimore, MD, USA: USENIX Association, 2018, pp. 1687-1704, ISBN: 9781931971461.

[14] Z. Berkay Celik, Patrick McDaniel, and Gang Tan, "SOTERIA: Automated IoT Safety and Security Analysis", in: *Proceedings of the 2018 USENIX Conference on Usenix Annual Technical Conference*, USENIX ATC '18, Boston, MA, USA: USENIX Association, 2018, pp. 147-158, ISBN: 9781931971447.

[15] Arthur Charguéraud, "Pretty-big-step semantics", in: *Proceedings of the 22nd European Symposium on Programming (ESOP 2013)*, Springer, 2013, pp. 41-60.
[16] Arthur Charguéraud, Alan Schmitt, and Thomas Wood, "JSExplain: A Double Debugger for JavaScript", in: *The Web Conference 2018*, Lyon, France, 2018, pp. 1-9, DOI: 10.1145/3184558.3185969.

[17] Xiaohong Chen, Zhengyao Lin, Minh-Thai Trinh, and Grigore Rosu, "Towards a Trustworthy Semantics-Based Language Framework via Proof Generation", in: *Computer Aided Verification*, ed. by Alexandra Silva and K. Rustan M. Leino, Cham: Springer International Publishing, 2021, pp. 477-499, ISBN: 978-3-030-81688-9.

[18] *COMPCERT*, URL: https://compcert.org.

[19] *Coq Program Extraction*, URL: https://coq.inria.fr/refman/addendum/extraction.html.

[20] *ECMA, ECMAScript 2021 Language Specification*, 2021, URL: https://tc39.es/ecma262/2021/.

[21] Chucky Ellison and Grigore Rosu, "An Executable Formal Semantics of C with Applications", in: *Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages*, POPL '12, Philadelphia, PA, USA: Association for Computing Machinery, 2012, pp. 533-544, ISBN: 9781450310833, DOI: 10.1145/2103656.2103719, URL: https://doi.org/10.1145/2103656.2103719.

[22] *engine262, An implementation of ECMA-262 in JavaScript*, URL: https://github.com/engine262/engine262.

[23] Daniele Filaretti and Sergio Maffeis, "An Executable Formal Semantics of PHP", in: *ECOOP 2014 – Object-Oriented Programming*, ed. by Richard Jones, Berlin, Heidelberg: Springer Berlin Heidelberg, 2014, pp. 567-592, ISBN: 978-3-662-44202-9.

[24] Cormac Flanagan, Amr Sabry, Bruce F. Duba, and Matthias Felleisen, "The Essence of Compiling with Continuations", in: *Proceedings of the ACM SIGPLAN'93 Conference on Programming Language Design and Implementation (PLDI)*, Albuquerque, New Mexico, USA, June 23-25, 1993, ed. by Robert Cartwright, ACM, 1993, pp. 237-247, ISBN: 0-89791-598-4, DOI: 10.1145/155090.155113, URL: https://doi.org/10.1145/155090.155113.
[25] Arjun Guha, Claudiu Saftoiu, and Shriram Krishnamurthi, "The Essence of JavaScript", in: *ECOOP, Lecture Notes in Computer Science* (June 2010), pp. 126–150, DOI: 10.1007/978-3-642-14107-2_7.

[26] John Hannan and Dale Miller, "From Operational Semantics to Abstract Machines: Preliminary Results", in: *Proceedings of the 1990 ACM Conference on LISP and Functional Programming*, LFP '90, Nice, France: Association for Computing Machinery, 1990, pp. 323–332, ISBN: 089791368X, DOI: 10.1145/91556.91680, URL: https://doi.org/10.1145/91556.91680.

[27] Robert Harper, Furio Honsell, and Gordon Plotkin, "A Framework for Defining Logics", in: *J. ACM* 40.1 (1993), pp. 143–184, ISSN: 0004-5411, DOI: 10.1145/138027.138060, URL: https://doi.org/10.1145/138027.138060.

[28] Chris Hathhorn, Chucky Ellison, and Grigore Roșu, "Defining the Undefinedness of C", in: *Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation*, PLDI '15, Portland, OR, USA: Association for Computing Machinery, 2015, pp. 336–345, ISBN: 9781450334686, DOI: 10.1145/2737924.2737979, URL: https://doi.org/10.1145/2737924.2737979.

[29] HOL, URL: https://hol-theorem-prover.org/.

[30] Isabelle, URL: https://isabelle.in.tum.de.

[31] Roshan P. James, A. U.S., and A. Sabry, "Yield: Mainstream Delimited Continuations", in: 2011.

[32] Gilles Kahn, "Natural Semantics", in: *Proceedings of the 4th Annual Symposium on Theoretical Aspects of Computer Science*, STACS '87, Berlin, Heidelberg: Springer-Verlag, 1987, pp. 22–39, ISBN: 354017219X.

[33] Adam Khayam, Louis Noizet, and Alan Schmitt, "A Faithful Description of ECMAScript Algorithms", in: *Proceedings of the 24th International Symposium on Principles and Practice of Declarative Programming*, PPDP '22, Tbilisi, Georgia: Association for Computing Machinery, 2022, ISBN: 9781450397032, DOI: 10.1145/3551357.3551381, URL: https://doi.org/10.1145/3551357.3551381.

[34] Adam Khayam, Louis Noizet, and Alan Schmitt, "JSkel: Towards a Formalization of JavaScript's Semantics", in: *JFLA 2021 - Journées Francophones des Langages Applicatifs*, Virtuelles, France, Apr. 2021, pp. 1–22, URL: https://hal.inria.fr/hal-03509431.
[35] Adam Khayam and Alan Schmitt, *A Practical Approach for Describing Language Semantics*, Submitted for publication - The Art, Science, and Engineering of Programming, May 2022.

[36] Casey Klein, John Clements, Christos Dimoulas, Carl Eastlund, Matthias Felleisen, Matthew Flatt, Jay A. McCarthy, Jon Rafkind, Sam Tobin-Hochstadt, and Robert Bruce Findler, “Run Your Research: On the Effectiveness of Lightweight Mechanization”, in: *SIGPLAN Not.* 47.1 (2012), pp. 285–296, ISSN: 0362-1340, DOI: 10.1145/2103621.2103691, URL: https://doi.org/10.1145/2103621.2103691.

[37] Ramana Kumar, Magnus O. Myreen, Michael Norrish, and Scott Owens, “CakeML: A Verified Implementation of ML”, in: *Principles of Programming Languages (POPL)*, ACM Press, Jan. 2014, pp. 179–191, DOI: 10.1145/2535838.2535841, URL: https://cakeml.org/popl14.pdf.

[38] Peter J. Landin, “The Mechanical Evaluation of Expressions”, in: *Comput. J.* 6 (1964), pp. 308–320.

[39] Xavier Leroy, “Formal Verification of a Realistic Compiler”, in: *Commun. ACM* 52.7 (July 2009), pp. 107–115, ISSN: 0001-0782, DOI: 10.1145/1538788.1538814, URL: https://doi.org/10.1145/1538788.1538814.

[40] Liyi Li and Elsa L. Gunter, “A Complete Semantics of K and Its Translation to Isabelle”, in: *Theoretical Aspects of Computing – ICTAC 2021: 18th International Colloquium, Virtual Event, Nur-Sultan, Kazakhstan, September 8–10, 2021, Proceedings*, Berlin, Heidelberg: Springer-Verlag, 2021, pp. 152–171, ISBN: 978-3-030-85314-3, DOI: 10.1007/978-3-030-85315-0_10, URL: https://doi.org/10.1007/978-3-030-85315-0_10.

[41] Noizet Louis and Schmitt Alan, “Semantics in Skel and Necro”, in: *Italian Conference on Theoretical Computer Science, Rome, Italy, September 7-9, 2022*, 2022.

[42] Enzo Crance Martin Bodin Nathanael Courant and Louis Noizet, *Necro Ocaml Generator*, https://gitlab.inria.fr/skeletons/necro-ml, URL: https://gitlab.inria.fr/skeletons/necro-ml.

[43] Robert Milne and C. Strachey, *A Theory of Programming Language Semantics*, 99th, USA: Halsted Press, 1977, ISBN: 0470989068.

[44] Robin Milner, Mads Tofte, and David Macqueen, *The Definition of Standard ML*, Cambridge, MA, USA: MIT Press, 1997, ISBN: 0262631814.
[45] Raphaël Monat, “Static Type and Value Analysis by Abstract Interpretation of Python Programs with Native C Libraries”, PhD thesis, Sorbonne University, 2021.

[46] Peter D Mosses, “Modular structural operational semantics”, in: *The Journal of Logic and Algebraic Programming* 60-61 (2004), Structural Operational Semantics, pp. 195–228, ISSN: 1567-8326, DOI: https://doi.org/10.1016/j.jlap.2004.03.008, URL: https://www.sciencedirect.com/science/article/pii/S156783260400027X.

[47] Dominic P. Mulligan, Scott Owens, Kathryn E. Gray, Tom Ridge, and Peter Sewell, “Lem: Reusable Engineering of Real-World Semantics”, in: *Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming*, ICFP ’14, Gothenburg, Sweden: Association for Computing Machinery, 2014, pp. 175–188, ISBN: 9781450328739, DOI: 10.1145/2628136.2628143, URL: https://doi.org/10.1145/2628136.2628143.

[48] Magnus O. Myreen and Scott Owens, “Proof-Producing Synthesis of ML from Higher-Order Logic”, in: *SIGPLAN Not.* 47.9 (2012), pp. 115–126, ISSN: 0362-1340, DOI: 10.1145/2398856.2364545, URL: https://doi.org/10.1145/2398856.2364545.

[49] Louis Noizet, *Necro Debugger Generator*, https://gitlab.inria.fr/skeletons/necro-debug, URL: https://gitlab.inria.fr/skeletons/necro-debug.

[50] Louis Noizet, *Necro Gallina Generator*, https://gitlab.inria.fr/skeletons/necro-coq, URL: https://gitlab.inria.fr/skeletons/necro-coq.

[51] Louis Noizet, *Necro Library*, https://gitlab.inria.fr/skeletons/necro, URL: https://gitlab.inria.fr/skeletons/necro.

[52] Louis Noizet and Alan Schmitt, “Semantics in Skel and Necro”, in: *ICTCS 2022 - Italian Conference on Theoretical Computer Science*, CEUR Workshop Proceedings, Rome, Italy, Sept. 2022, pp. 1–17, URL: https://hal.inria.fr/hal-03784478.

[53] Louis Noizet and Alan Schmitt, *Stating and Handling Semantics with Skel and Necro*, Research Report RR-9449, Inria Rennes - Bretagne Atlantique, Jan. 2022, pp. 1–23, URL: https://hal.inria.fr/hal-03543701.

[54] Louis Noizet and Alan Schmitt, *Stating and Handling Semantics with Skel and Necro*, Research Report, Inria Rennes - Bretagne Atlantique, Jan. 2022, p. 20, URL: https://hal.inria.fr/hal-03543701.
[55] Scott Owens, Peter Böhm, Francesco Zappa Nardelli, and Peter Sewell, “Lem: A Lightweight Tool for Heavyweight Semantics”, in: *Interactive Theorem Proving*, ed. by Marko van Eekelen, Herman Geuvers, Julien Schmaltz, and Freek Wiedijk, Berlin, Heidelberg: Springer Berlin Heidelberg, 2011, pp. 363–369, ISBN: 978-3-642-22863-6.

[56] Daejun Park, Andrei Stefănescu, and Grigore Roşu, “KJS: A Complete Formal Semantics of JavaScript”, in: *ACM SIGPLAN Notices* 50 (June 2015), pp. 346–356, DOI: 10.1145/2813885.2737991.

[57] Jihyeok Park, Seungmin An, and Sukyoung Ryu, “Automatically Deriving JavaScript Static Analyzers from Specifications Using Meta-Level Static Analysis”, in: *Proceedings of the 30th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering*, ESEC/FSE 2022, Singapore, Singapore: Association for Computing Machinery, 2022, pp. 1022–1034, ISBN: 9781450394130, DOI: 10.1145/3540250.3549097, URL: https://doi.org/10.1145/3540250.3549097.

[58] Jihyeok Park, Seungmin An, Wonho Shin, Yusung Sim, and Sukyoung Ryu, “JS-TAR: JavaScript Specification Type Analyzer using Refinement”, in: *2021 36th IEEE/ACM International Conference on Automated Software Engineering (ASE)*, 2021, pp. 606–616, DOI: 10.1109/ASE51524.2021.9678781.

[59] Jihyeok Park, Jihee Park, Seungmin An, and Sukyoung Ryu, “JISET: JavaScript IR-based Semantics Extraction Toolchain”, in: *2020 35th IEEE/ACM International Conference on Automated Software Engineering (ASE)*, 2020, pp. 647–658.

[60] Blaise Pascal, *The Provincial Letters*, 1657.

[61] Gordon D Plotkin, *A structural approach to operational semantics*, Aarhus university, 1981.

[62] Gordon D. Plotkin, “LCF Considered as a Programming Language”, in: *Theoretical Computer Science* 5.3 (1977), pp. 223–255, DOI: 10.1016/0304-3975(77)90044-5, URL: https://doi.org/10.1016/0304-3975(77)90044-5.

[63] Grigore Roşu and Traian Şerbănuţă, “An Overview of the K Semantic Framework”, in: *The Journal of Logic and Algebraic Programming* 79 (Aug. 2010), pp. 397–434, DOI: 10.1016/j.jlap.2010.03.012.
[64] Amr Sabry and Matthias Felleisen, "Reasoning About Programs in Continuation-Passing Style", in: *Proceedings of the Conference on Lisp and Functional Programming*, LFP 1992, San Francisco, California, USA, 22-24 June 1992, ed. by Jon L. White, ACM, 1992, pp. 288-298, ISBN: 0-89791-481-3, DOI: 10.1145/141471.141563, URL: https://doi.org/10.1145/141471.141563.

[65] Manuel Serrano, *Hop, multitier Web Programming*, 2006, URL: http://hop.inria.fr.

[66] Peter Sewell, Francesco Zappa Nardelli, Scott Owens, Gilles Peskine, Thomas Ridge, Susmit Sarkar, and Rok Strniša, "Ott: Effective Tool Support for the Working Semanticist", in: *Proceedings of the 12th ACM SIGPLAN International Conference on Functional Programming*, ICFP '07, Freiburg, Germany: Association for Computing Machinery, 2007, pp. 1-12, ISBN: 9781595938152, DOI: 10.1145/1291151.1291155, URL: https://doi.org/10.1145/1291151.1291155.

[67] KC Sivaramakrishnan, Stephen Dolan, Leo White, Tom Kelly, Sadiq Jaffer, and Anil Madhavapeddy, "Retrofitting Effect Handlers onto OCaml", in: *Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation*, PLDI 2021, Virtual, Canada: Association for Computing Machinery, 2021, pp. 206-221, ISBN: 9781450383912, DOI: 10.1145/3453483.3454039, URL: https://doi.org/10.1145/3453483.3454039.

[68] *Standard ML Family GitHub Project*, URL: https://smlfamily.github.io.

[69] Yong Kiam Tan, Scott Owens, and Ramana Kumar, "A Verified Type System for CakeML", in: *IFL '15, Koblenz, Germany: Association for Computing Machinery*, 2015, ISBN: 9781450342735, DOI: 10.1145/2897336.2897344, URL: https://doi.org/10.1145/2897336.2897344.

[70] *The Coq proof assistant*, URL: https://coq.inria.fr.

[71] *The Twelf Project*, URL: http://twelf.org/wiki/Main_Page.

[72] Philip Wadler, "The Essence of Functional Programming", in: *Conference Record of the Nineteenth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages*, Albuquerque, New Mexico, USA, January 19-22, 1992, pp. 1-14, DOI: 10.1145/143165.143169, URL: https://doi.org/10.1145/143165.143169.
[73] C.P. Wadsworth, *Semantics and Pragmatics of the Lambda-calculus*, University of Oxford, 1971.

[74] Qi Wang, Wajih Hassan, Adam Bates, and Carl Gunter, “Fear and Logging in the Internet of Things”, in: Jan. 2018, DOI: 10.14722/ndss.2018.23291.