[More Detail] [Collapse All]
Feature: Pre-emptive Scheduler

  Pre-emptive schedule feature allows a process to call an other
  process asyncrhoronously.

  Pre-emptive scheduling:
  - two entries are put into the scheduling sequence +steps+.
    First entry schedules the called process, and second entry
    resumes back to caller process. 
 -  the location of thes two entries is chosen non-deterministally, but
    call and resume are always two successive steps so that caller      
    may access response from the called process


 Implementation uses +resume_context+ variable to flag state of the
 caller process: scheduling, resuming, and normal call.

 Pseudo code of caller process:

 procedure caller() {

     // resume_context <> nil
     if resuming then
          // Modify stack to return to point of schedulig
          stack := +resume_context+;
         return;
     end

     ...
     // Schedule call
     call schedule_process( process, input );
     // Either scheduling or resuming
 resuming:
      if ( resume_context=Nil ) then
         // scheduling
         goto exit;
         end
         
      // resuming: clear resume status, access response
      resume_context := NIl
      if ( InfrastructureServiceGetStatus( process ) ) {
          InfrastructureServiceGetResponse( process ) 
      }
          

      ...

 exit:
    return:
 }
features/300-scheduler/100-pre-emptive-schedule.feature
- Background: Create application
link

Define three interfaces '/max2(post)', and '/set1(post)', '/dummy(post)'.

Services '/max2(post)', and '/set1(post)' are implemented later in
scenarios. Service '/dummy(post)' is no operation.

Memory location 'mem' is inialized with 0

Invariant 'alwaysLessThan2' verifies that value in 'mem' should
remain always <= 2.
features/300-scheduler/100-pre-emptive-schedule.feature:54
When I successfully run `sbuilder.rb init`
And a file named "cnf/sbuilder.yaml" with:
#
# Define interfaces

interfaces:
    -  className: Sbuilder::ParamSetLoaderSwagger
       file: example_interface.yaml
And a file named "cnf/example_interface.yaml" with:
swagger: "2.0"
info:
 version: 1.0.0
 title: Sbuilder.rb example walk-trough
 description: A scheduler example
host: localhost
basePath: /api
schemes:
 - http
consumes:
 - application/json
produces:
 - application/json
paths: {}
definitions: {}
And YAML configuration file `cnf/example_interface.yaml` in path `paths`

# Interface operation /max2(post) and /set1(post)

  /max2:
    post: 
      operationId: max2
      responses:
         200:
            description: OK
  /set1:
    post: 
      operationId: set1
      responses:
         200:
            description: OK

  /dummy:
    post: 
      operationId: dummy
      responses:
         200:
            description: OK
And YAML configuration file `cnf/sbuilder.yaml`
#
# Define domain resolvers in 'cnf/sbuilder.yaml'
#
resolvers:
      - url: cnf/resolver_default.yaml
Given a file named "cnf/resolver_default.yaml" with:
# resolver which catch-all matcher 

   -    Name: default-relsover
        Matcher: !ruby/regexp /.*/
        Rules: 
          - Matcher: !ruby/regexp /.*/
            Domain: default_domain
And YAML configuration file `cnf/sbuilder.yaml`
#
# setup extensions:
# - for interface implementation
# - steps to execute
#
setups:
  - setupDirectory: example
    desc: Example setup
    extensions:
      -  url: cnf/extend-steps.yaml
      # -  url: cnf/extend-implementation.yaml
And YAML configuration file `cnf/sbuilder.yaml`
#
# Map service implementation 

snippets:

  - className: Sbuilder::SnippetLoaderSimple 
    configuration:
        metatypes:
           code: Example code

    snippets:

      - metatype: service_implementation
        appName: /max2(post)
        file: max2_post.tla

      - metatype: service_implementation
        appName: /dummy(post)
        file: dummy_post.tla

      - metatype: code
        appName: max2
        file: max2.tla

      - metatype: service_implementation
        appName: /set1(post)
        file: set1_post.tla

      - metatype: code
        appName: set1
        file: set1.tla

      - metatype: code
        appName: mem
        file: mem.tla

      - metatype: framework-svc
        appName: alwaysLessThan2
        file: alwaysLessThan2.tla
And a file named "cnf/extend-steps.yaml" with:

# Define steps, which environment will take. In this case,
# environment call interface '/customer(post)', and because no
# input constaint is defined, environment uses all input
# combination for 'id', 'name', and 'type' parameters in the
# operation.
#
- step-extension:
       - interface: /max2(post)
       - interface: /dummy(post)
       - interface: /set1(post)
       - interface: /dummy(post)
       - interface: /set1(post)
       - interface: /dummy(post)
       - interface: /max2(post)
       - interface: /max2(post)
# ------------------------------------------------------------------
# Specification code
#
And a file named "src/mem.tla" with:
     {{#SPEC_NAME}}code.mem{{/SPEC_NAME}} = 0; 
And a file named "src/dummy_post.tla" with:
\* dummy(post) - skip no operation
macro {{#SPEC_NAME}}service_implementation./dummy(post){{/SPEC_NAME}}( input ) {
    skip;
}
And a file named "src/max2_post.tla" with:
\* max2_post
macro {{#SPEC_NAME}}service_implementation./max2(post){{/SPEC_NAME}}( input ) {

   print << "Input", input >>;
   call {{#SPEC_NAME}}code.max2{{/SPEC_NAME}}( input );
}
And a file named "src/set1_post.tla" with:
\* set1_post:
macro {{#SPEC_NAME}}service_implementation./set1(post){{/SPEC_NAME}}( input ) {
   print << "Input", input >>;
   call {{#SPEC_NAME}}code.set1{{/SPEC_NAME}}( input );
}
And a file named "src/alwaysLessThan2.tla" with:
\* alwaysLessThan2 invariant
alwaysLessThan2 == {{#SPEC_NAME}}code.mem{{/SPEC_NAME}} <= 2
And YAML configuration file `cnf/sbuilder.yaml`
#
# mem variable must remain always less than 2
# - set1 : sets it to 1
# - max2 : checks that it is before incrementing it
#
invariants:
      - alwaysLessThan2: set1 sets to 1, max2 check zero before adding 2
- Scenario: No interleavig - invariat respected
link

In this scenario:
- max2 checks that +mem+ = 0 before incrementing it by 2
- set1 sets +mem+ to 1 (no incrementing)

Invariant 'alwaysLessThan2' is satisfied
features/300-scheduler/100-pre-emptive-schedule.feature:270
Given a file named "src/max2.tla" with:
\* max2:
procedure  {{#SPEC_NAME}}code.max2{{/SPEC_NAME}}( input ) {
   {{#SPEC_NAME}}code.max2{{/SPEC_NAME}}_start:

        if ( {{#SPEC_NAME}}code.mem{{/SPEC_NAME}} = 0 ) {
            {{#SPEC_NAME}}code.mem{{/SPEC_NAME}} := {{#SPEC_NAME}}code.mem{{/SPEC_NAME}} + 2;
        }
        else {
            {{#SPEC_NAME}}code.mem{{/SPEC_NAME}} := 0;
        };
   {{#SPEC_NAME}}code.max2{{/SPEC_NAME}}_end:
       return;
}
And a file named "src/set1.tla" with:
\* set1:
procedure  {{#SPEC_NAME}}code.set1{{/SPEC_NAME}}( input ) {

   {{#SPEC_NAME}}code.set1{{/SPEC_NAME}}_start:
        {{#SPEC_NAME}}code.mem{{/SPEC_NAME}} := 1;
   {{#SPEC_NAME}}code.set1{{/SPEC_NAME}}_end:
       return;
}
When I successfully run `sbuilder.rb generate example`
And I cd to "gen/example/tla"
And I successfully run command `java -cp $TLATOOLS pcal.trans model`
And I run command `java -cp $TLATOOLS tlc2.TLC setup`
And the stdout should contain "Model checking completed. No error has been found."
- Scenario: Interleavig - invariant violated
link

In this scenario:
- max2
  -- checks that +mem+ = 0
  -- makes an external call, and max2 to pre-empt
  -- scheduler schedules some other process, including +set1+
  -- when max2 resumes, +mem+ has changed to 1
  -- adding to +mem+ in this case results value 3 in +mem+
- set1 sets +mem+ to 1 (no incrementing)

Notice, however that local variable local_to_has correct value


Invariant 'alwaysLessThan2' is violated
features/300-scheduler/100-pre-emptive-schedule.feature:313
Given a file named "src/max2.tla" with:
\* max2:
\* max2_post
procedure  {{#SPEC_NAME}}code.max2{{/SPEC_NAME}}( input ) 
      variable max2_local = 1 ; 
{

   {{#SPEC_NAME}}code.max2{{/SPEC_NAME}}_resume:

         \* check first if resuming 
         if ( resume_context # Nil ) {
            \* modify stack entry with resum context
            stack := <<resume_context.ret_ctx >> \o stack[self];
  {{#SPEC_NAME}}code.max2{{/SPEC_NAME}}_resumed:
             \* continue procssing in context on top the stack
             return;
         };

   {{#SPEC_NAME}}code.max2{{/SPEC_NAME}}_start:
        max2_local := max2_local + {{#SPEC_NAME}}code.mem{{/SPEC_NAME}};
        if ( {{#SPEC_NAME}}code.mem{{/SPEC_NAME}} = 0 ) {

            assert( max2_local = 1 );
            \* exteral call - causes pre-emptive scheduling
     call schedule_process_proc( [ called |-> "p__dummy_post_", input |-> Nil ] );

  {{#SPEC_NAME}}code.max2{{/SPEC_NAME}}_back:
            assert( max2_local = 1 );

            \* if scheduling: resume_context = Nil
            if ( resume_context = Nil ) {
               goto {{#SPEC_NAME}}code.max2{{/SPEC_NAME}}_end;
            };

            \* here resumed - clear resume context and continue 'normally'
  {{#SPEC_NAME}}code.max2{{/SPEC_NAME}}_continue:
            assert( max2_local = 1 );
     resume_context := Nil ;

            {{#SPEC_NAME}}code.mem{{/SPEC_NAME}} := {{#SPEC_NAME}}code.mem{{/SPEC_NAME}} + 2;
        }
        else {
            assert( max2_local > 1 );
            {{#SPEC_NAME}}code.mem{{/SPEC_NAME}} := 0;
        };
   {{#SPEC_NAME}}code.max2{{/SPEC_NAME}}_end:
       return;
}
And a file named "src/set1.tla" with:
\* set1:
procedure  {{#SPEC_NAME}}code.set1{{/SPEC_NAME}}( input ) {

   {{#SPEC_NAME}}code.set1{{/SPEC_NAME}}_start:
        {{#SPEC_NAME}}code.mem{{/SPEC_NAME}} := 1;
   {{#SPEC_NAME}}code.set1{{/SPEC_NAME}}_end:
       return;
}
When I successfully run `sbuilder.rb generate example`
And I cd to "gen/example/tla"
And I successfully run command `java -cp $TLATOOLS pcal.trans model`
And I run command `java -cp $TLATOOLS tlc2.TLC setup`
Then the stdout should contain "Invariant alwaysLessThan2 is violated."