Analysis-Specific Settings

Here we discuss analysis-specific configuration.

Memory Anomalies

Locating memory anomalies or evaluating their effects requires to:

  1. Configure the environment, as we describe in ScEpTIC Configuration

  2. Set run_locate_memory_test and/or run_evaluate_memory_test to True, accordingly to the test we wish to execute

  3. Set the execution_depth parameter, as we describe in Execution Depth

Input Accesses

Input access analysis requires to:

  1. Configure the environment, as we describe in ScEpTIC Configuration

  2. Set run_input_consistency_test to True

  3. Create the input functions, as we describe in Inputs

  4. Set the consistency model of each input function

Input Accesses - Input Access Model

To set the consistency model of an input function, we need to use the set_consistency_model(input_name, consistecy_model) class method that the InputManager exposes:

  • input_name corresponds to the name of the input function

  • consistency_model corresponds to the consistency model we want for the input

    • If we desire a most recent access model, we set it to InputManager.MOST_RECENT

    • If we desire a long term access model, we set it to InputManager.LONG_TERM

For example, we can require a most recent access model for a temperature sensor as follows:

from ScEpTIC.emulator.io.input import InputManager

InputManager.create_input('DHT-11', 'input', 'i32')
InputManager.set_input_value('DHT-11', '23')
InputManager.set_consistency_model('DHT-11', InputManager.MOST_RECENT)

Output Accesses

Output access analysis requires to:

  1. Configure the environment, as we describe in ScEpTIC Configuration

  2. Set run_output_profiling to True

  3. Create the output functions that represents the environment, as we describe in Outputs

  4. Set the idempotency model of each output function

Output Accesses - Output Idempotency Model

We can set the output idempotency model using two class methods that the OutputManager exposes:

  • set_default_idempotent(default_idempotent) sets if the default idempotency model is idempotent (default_idempotent = True) or non-idempotent (default_idempotent = False). Note that ScEpTIC sets the output idempotency when an output function is created, so we need to specify the default output idempotency before defining output functions

  • set_idempotency(output_name, idempotency_model) sets the idempotency model of the considered output

    • output_name corresponds to the name of the output function

    • idempotency_model corresponds to the idempotency model we want for the output

      • If we desire a idempotent model, we set it to OutputManager.IDEMPOTENT

      • If we desire a non-idempotent model, we set it to OutputManager.NON_IDEMPOTENT

For example, we can require a non-idempotent access model for a servo as follows:

from ScEpTIC.emulator.io.output import OutputManager, OutputSkeleton

OutputManager.set_default_idempotent(True)

class Servo(OutputSkeleton):

    def output_init(self):
        self.set_output_val(0)

    def get_val(self):
        value = self.get_output_val() + self.args[0]

        if value >= 360:
            value = 0

        self.set_output_val(value)
        return None

Servo.define_output('SERVO', 'move_servo', 'i32', 'void')

OutputManager.set_idempotency('SERVO', OutputManager.NON_IDEMPOTENT)

Continuous Execution

ScEpTIC allows us to execute the program in a continuous execution (i.e. as it would happens with a reliable and stable power supply). This can be useful to retrieve the continuous state of the program, at the end of its execution, or to debug the program execution (e.g. using printf()).

To execute the program continously, we just need to:

  1. Configure the environment, as we describe in ScEpTIC Configuration

  2. Set run_continuous to True

Custom Intermittent Execution

ScEpTIC allows us to profile and debug specific intermittent executions of a program, by exposting C function calls that allows us to reproduce specific power failures and to log events or variables content. This analysis produces an execution trace with the events of interest, which we can then inspect to identify errors or unexpected behaviours.

To execute this analysis, we just need to: 1. Configure the environment, as we describe in ScEpTIC Configuration 2. Set run_profiling to True 3. Use the builtins that ScEpTIC exposes, directly in our C source code

ScEpTIC exposes the following builtins.

Log Events

sceptic_log(identifier, element); allows us to track events and the evolution of variable contents. It takes two arguments:

  • identifier consists in a string representing an arbitrary information on the event of interest

  • element consists in a variable we want to log. Note that this is optional and can be omitted

For example, we can log the content of a variable a with sceptic_log("a", a);, or we can signal the execution of a portion of code with sceptic_log("branch A executed");.

Generate Power Failures

sceptic_reset(mode, val) allows us to reproduce specific power failures. It takes two arguments:

  • mode is a string that indices how ScEpTIC controls the generation of the power failure when it executes sceptic_reset. It can be:

    • once: ScEpTIC simulates the power failure only the first time it encounters the function call

    • clock: ScEpTIC simulates the power failure if the reset logical clock is equal to the specified value. Note that ScEpTIC re-initializes the reset logical clock at system startup and every time it encounters a checkpoint, and increments it every time it simulates a power failure

    • conditional: ScEpTIC simulates the power failure only if the value parameter evaluates to True. Note that the power failures is generated only once

  • value specifies the optional conditions on whether to generate the power failure

For example, let us consider the following program:

01. checkpoint();
02. for(int i = 0; i < 10; i++) {
03.    // BLOCK A
04.    sceptic_reset("clock", 1);
05.
06.    // BLOCK B
07.    sceptic_reset("once");
08.
09.    // BLOCK C
10.    sceptic_reset("conditional", i > 8);
11. }

Here ScEpTIC generates a power failure at line 7, then a power failure at line 4, and finally a power failure at line 10 when i is equal to 9.

Change Input Values

sceptic_change_input(input_name, value) allows us to change the value of an input, during the program execution. It takes two arguments:

  • input_name is a string that represents the name of the input, as we defined in ScEpTIC configuration

  • value represents the new value of the input

Note that we can sceptic_change_input() in combination with the definition of sceptic_before_restore(), sceptic_after_restore(), sceptic_before_checkpoint(), and sceptic_after_checkpoint(), which we already describe in Program Configuration. For example, we can change the input value of a temperature sensor whenever a power failure happens as follows:

void sceptic_after_restore() {
    sceptic_change_input("Temperature", rand());
}

Note that we need to insert this code in our program source code.