Systems Programming

Type Contracts in Ada 2012 and SPARK 2014

Systems Programming – What is it?

  • Bare metal programming

    • bare board applications (no Operating System)
    • Operating Systems (ex: Muen separation kernel)
    • device drivers (ex: Ada Drivers Library)
    • communication stacks (ex: AdaCore TCP/IP stack)
  • Specifics of Systems Programming

    • direct access to hardware: registers, memory, etc.
    • side-effects (yes!)
    • efficiency is paramount (sometimes real-time even)
    • hard/impossible to debug

Systems Programming – How can SPARK help?

  • SPARK is a Systems Programming language

    • same features as Ada for accessing hardware (representation clauses, address clauses)
    • as efficient as Ada or C
  • Side-effects can be modeled in SPARK

    • reads and writes to memory-mapped devices are modeled
    • concurrent interactions with environment are modeled
  • SPARK can help catch problems by static analysis

    • correct flows, initialization, concurrent accesses
    • absence of run-time errors and preservation of invariants

Systems Programming – A trivial example

package Show_Trivial_Sys_Prog is Y : Integer; -- Y'Address could be replaced by any -- external address X : Integer with Volatile, Address => Y'Address; procedure Get (Val : out Integer) with Global => (In_Out => X), Depends => (Val => X, X => X); end Show_Trivial_Sys_Prog;
package body Show_Trivial_Sys_Prog is procedure Get (Val : out Integer) is begin Val := X; end Get; end Show_Trivial_Sys_Prog;
  • Comments:

    • X is volatile
    • X is also an output; output X depends on input X
    • X is only read

Volatile Variables and Volatile Types

  • Variables whose reads/writes cannot be optimized away

  • Identified through multiple aspects (or pragmas)

    • aspect Volatile
    • but also aspect Atomic
    • and GNAT aspect Volatile_Full_Access
    • all the above aspects can be set on type or object
  • Other aspects are useful on volatile variables

    • aspect Address to specify location in memory
    • aspect Import to skip definition/initialization
type T is new Integer with Volatile;

X : Integer with Atomic, Import, Address => ... ;

Flavors of Volatile Variables

Using Async_Readers / Async_Writers

  • Boolean aspects describing asynchronous behavior

    • Async_Readers if variable may be read asynchronously
    • Async_Writers if variable may be written asynchronously
  • Effect of Async_Readers on flow analysis

  • Effect of Async_Writers on flow analysis & proof

    • always initialized, always has an unknown value
package Volatile_Vars is pragma Elaborate_Body; Ext : array (1 .. 2) of Integer; X : Integer with Volatile, Address => Ext (1)'Address, Async_Readers; Y : Integer with Volatile, Address => Ext (2)'Address, Async_Writers; procedure Set; end Volatile_Vars;
package body Volatile_Vars is procedure Set is U, V : constant Integer := Y; begin pragma Assert (U = V); X := 0; X := 1; end Set; begin Ext := (others => 0); end Volatile_Vars;
with Volatile_Vars; procedure Show_Volatile_Vars is begin Volatile_Vars.Set; end Show_Volatile_Vars;

Using Effective_Reads / Effective_Writes

  • Boolean aspects distinguishing values & sequences

    • Effective_Reads if reading the variable has an effect on its value
    • Effective_Writes if writing the variable has an effect on its value
  • Effect of both on proof and flow dependencies

    • Final value of variable is seen as a sequence of values it took
package Volatile_Vars is pragma Elaborate_Body; Ext : array (1 .. 2) of Integer; X : Integer with Volatile, Address => Ext (1)'Address, Async_Readers, Effective_Writes; Y : Integer with Volatile, Address => Ext (2)'Address, Async_Writers, Effective_Reads; procedure Set with Depends => (X => Y, Y => Y); end Volatile_Vars;
package body Volatile_Vars is procedure Set is begin X := Y; X := 0; end Set; begin Ext := (others => 0); end Volatile_Vars;
with Volatile_Vars; procedure Show_Volatile_Vars is begin Volatile_Vars.Set; end Show_Volatile_Vars;

Combinations of Flavors of Volatile Variables

  • All four flavors can be set independently

    • Default for Volatile/Atomic is all four True
    • When some aspects set, all others default to False
  • Only half the possible combinations are legal

    • Async_Readers and/or Async_Writers is set
    • Effective_Reads = True forces Async_Writers = True
    • Effective_Writes = True forces Async_Readers = True
    • sensor: AW=True
    • actuator: AR=True
    • input port: AW=True, ER=True
    • output port: AR=True, EW=True

Constraints on Volatile Variables

  • Volatile variables must be defined at library level

  • Expressions (and functions) cannot have side-effects

    • read of variable with AW=True must appear alone on rhs of assign
    • a function cannot read a variable with ER=True
package Volatile_Vars is pragma Elaborate_Body; Ext : array (1 .. 4) of Integer; AR : Integer with Volatile, Address => Ext (1)'Address, Async_Readers; AW : Integer with Volatile, Address => Ext (2)'Address, Async_Writers; ER : Integer with Volatile, Address => Ext (3)'Address, Async_Writers, Effective_Reads; EW : Integer with Volatile, Address => Ext (4)'Address, Async_Readers, Effective_Writes; procedure Read_All; function Read_ER return Integer; procedure Set (V : Integer); end Volatile_Vars;
package body Volatile_Vars is procedure Read_All is Tmp : Integer := 0; begin Tmp := Tmp + AR; Tmp := Tmp + AW; EW := Tmp; Set (ER); end Read_All; function Read_ER return Integer is Tmp : Integer := ER; begin return Tmp; end Read_ER; procedure Set (V : Integer) is begin AW := V; end Set; begin Ext := (others => 0); end Volatile_Vars;
with Volatile_Vars; procedure Show_Volatile_Vars is V : Integer; begin Volatile_Vars.Read_All; V := Volatile_Vars.Read_ER; end Show_Volatile_Vars;
  • Comments:

    • AW not alone on rhs
    • ER not alone on rhs
    • ER output of Read_ER

Constraints on Volatile Functions

  • Functions should have mathematical interpretation

    • a function reading a variable with AW=True is marked as volatile with aspect Volatile_Function
    • calls to volatile functions are restricted like reads of Async_Writers
package Volatile_Vars is pragma Elaborate_Body; Ext : array (1 .. 4) of Integer; AR : Integer with Volatile, Address => Ext (1)'Address, Async_Readers; AW : Integer with Volatile, Address => Ext (2)'Address, Async_Writers; ER : Integer with Volatile, Address => Ext (3)'Address, Async_Writers, Effective_Reads; EW : Integer with Volatile, Address => Ext (4)'Address, Async_Readers, Effective_Writes; function Read_Non_Volatile return Integer; function Read_Volatile return Integer with Volatile_Function; function Read_ER return Integer with Volatile_Function; end Volatile_Vars;
package body Volatile_Vars is function Read_Non_Volatile return Integer is Tmp : Integer := 0; begin -- reads AR, AW, EW -- ERROR: not a volatile function Tmp := Tmp + AR; Tmp := Tmp + AW; Tmp := Tmp + EW; return Tmp; end Read_Non_Volatile; function Read_Volatile return Integer is Tmp : Integer := 0; begin -- reads AR, AW, EW -- OK for volatile function Tmp := Tmp + AR; Tmp := Tmp + AW; Tmp := Tmp + EW; return Tmp; end Read_Volatile; function Read_ER return Integer is Tmp : Integer := ER; begin -- reads ER -- ERROR: ER output of Read_ER return Tmp; end Read_ER; begin Ext := (others => 0); end Volatile_Vars;
with Volatile_Vars; procedure Show_Volatile_Vars is V : Integer; begin V := Volatile_Vars.Read_Non_Volatile; V := Volatile_Vars.Read_Volatile; V := Volatile_Vars.Read_ER; end Show_Volatile_Vars;

State Abstraction on Volatile Variables

  • Abstract state needs to be identified as External

  • Flavors of volatility can be specified

    • Default if none specified is all True
package P1 with Abstract_State => (S with External) is procedure Process (Data : out Integer) with Global => (In_Out => S); end P1;
package P2 with Abstract_State => (S with External => (Async_Writers, -- OK if refined into AW, ER Effective_Reads) -- not OK if refined into AR, EW ) is procedure Process (Data : out Integer) with Global => (In_Out => S); end P2;

Constraints on Address Attribute

  • Address of volatile variable can be specified
package Show_Address_Attribute is Ext : array (1 .. 2) of Integer; X : Integer with Volatile, Address => Ext (1)'Address; Y : Integer with Volatile; for Y'Address use Ext (2)'Address; end Show_Address_Attribute;
  • Address attribute not allowed in expressions

  • Overlays are allowed

    • GNATprove does not check absence of overlays
    • GNATprove does not model the resulting aliasing
procedure Show_Address_Overlay is X : Integer := 1; Y : Integer := 0 with Address => X'Address; pragma Assert (X = 1); -- assertion wrongly proved begin null; end Show_Address_Overlay;

Can something be known of volatile variables?

  • Variables with Async_Writers have no known value

  • ... but they have a known type!

    • type range, ex: 0 .. 360
    • type predicate, ex: 0 .. 15 | 17 .. 42 | 43 .. 360
  • Variables without Async_Writers have a known value

  • GNATprove also assumes all values are valid (X'Valid)

package Show_Provable_Volatile_Var is X : Integer with Volatile, Async_Readers; procedure Read_Value; end Show_Provable_Volatile_Var;
package body Show_Provable_Volatile_Var is procedure Read_Value is begin X := 42; pragma Assert (X = 42); -- proved! end Read_Value; end Show_Provable_Volatile_Var;

Other Concerns in Systems Programming

  • Software startup state ⟶ elaboration rules

    • SPARK follows Ada static elaboration model
    • ... with additional constraints for ensuring correct initialization
    • ... but GNATprove follows the relaxed GNAT static elaboration
  • Handling of faults ⟶ exception handling

    • raising exceptions is allowed in SPARK
    • ... but exception handlers are SPARK_Mode => Off
    • ... typically the last-chance-handler is used instead
  • Concurrency inside the application ⟶ tasking support

    • Ravenscar and Extended_Ravenscar profiles supported in SPARK

Code Examples / Pitfalls

Example #1

package Example_01 is Ext : Integer; X : Integer with Volatile, Address => Ext'Address; procedure Get (Val : out Integer) with Global => (Input => X), Depends => (Val => X); end Example_01;
package body Example_01 is procedure Get (Val : out Integer) is begin Val := X; end Get; end Example_01;

This code is not correct. X has Effective_Reads set by default, hence it is also an output.

Example #2

package Example_02 is Ext : Integer; X : Integer with Volatile, Address => Ext'Address, Async_Readers, Async_Writers, Effective_Writes; procedure Get (Val : out Integer) with Global => (Input => X), Depends => (Val => X); end Example_02;
package body Example_02 is procedure Get (Val : out Integer) is begin Val := X; end Get; end Example_02;

This code is correct. X has Effective_Reads = False, hence it is only an input.

Example #3

package Example_03 is Speed : Float with Volatile, Async_Writers; Motor : Float with Volatile, Async_Readers; procedure Adjust with Depends => (Motor =>+ Speed); end Example_03;
package body Example_03 is procedure Adjust is Cur_Speed : constant Float := Speed; begin if abs (Cur_Speed) > 100.0 then Motor := Motor - 1.0; end if; end Adjust; end Example_03;

This code is correct. Speed is an input only, Motor is both an input and output. Note how the current value of Speed is first copied to be tested in a larger expression.

Example #4

package Example_04 is Raw_Data : Float with Volatile, Async_Writers, Effective_Reads; Data : Float with Volatile, Async_Readers, Effective_Writes; procedure Smooth with Depends => (Data => Raw_Data); end Example_04;
package body Example_04 is procedure Smooth is Data1 : constant Float := Raw_Data; Data2 : constant Float := Raw_Data; begin Data := Data1; Data := (Data1 + Data2) / 2.0; Data := Data2; end Smooth; end Example_04;

This code is not correct. Raw_Data has Effective_Reads set, hence it is also an output.

Example #5

package Example_05 is type Regval is new Integer with Volatile; type Regnum is range 1 .. 32; type Registers is array (Regnum) of Regval; Regs : Registers with Async_Writers, Async_Readers; function Reg (R : Regnum) return Integer is (Integer (Regs (R))) with Volatile_Function; end Example_05;

This code is not correct. Regs has Async_Writers set, hence it cannot appear as the expression in an expression function.

Example #6

package Example_06 is type Regval is new Integer with Volatile; type Regnum is range 1 .. 32; type Registers is array (Regnum) of Regval; Regs : Registers with Async_Writers, Async_Readers; function Reg (R : Regnum) return Integer with Volatile_Function; end Example_06;
package body Example_06 is function Reg (R : Regnum) return Integer is V : Regval := Regs (R); begin return Integer (V); end Reg; end Example_06;

This code is not correct. Regval is a volatile type, hence variable V is volatile and cannot be declared locally.

Example #7

package Example_07 is type Regval is new Integer with Volatile; type Regnum is range 1 .. 32; type Registers is array (Regnum) of Regval; Regs : Registers with Async_Writers, Async_Readers; function Reg (R : Regnum) return Integer with Volatile_Function; end Example_07;
package body Example_07 is function Reg (R : Regnum) return Integer is begin return Integer (Regs (R)); end Reg; end Example_07;

This code is correct. Regs has Effective_Reads = False hence can be read in a function. Function Reg is marked as volatile with aspect Volatile_Function. No volatile variable is declared locally.

Example #8

package Example_08 with Abstract_State => (State with External), Initializes => State is procedure Dummy; end Example_08;
package body Example_08 with Refined_State => (State => (X, Y, Z)) is X : Integer with Volatile, Async_Readers; Y : Integer with Volatile, Async_Writers; Z : Integer := 0; procedure Dummy is begin null; end Dummy; end Example_08;

This code is not correct. X has Async_Writers = False, hence is not considered as always initialized. As aspect Initializes specifies that State should be initialized after elaboration, this is an error. Note that is allowed to bundle volatile and non-volatile variables in an external abstract state.

Example #9

package Example_09 is type Pair is record U, V : Natural; end record with Predicate => U /= V; X : Pair with Atomic, Async_Readers, Async_Writers; function Max return Integer with Volatile_Function, Post => Max'Result /= 0; end Example_09;
package body Example_09 is function Max return Integer is Val1 : constant Natural := X.U; Val2 : constant Natural := X.V; begin return Natural'Max (Val1, Val2); end Max; end Example_09;

This code is not correct. X has Async_Writers set, hence it may have been written between the successive reads of X.U and X.V.

Example #10

package Example_10 is type Pair is record U, V : Natural; end record with Predicate => U /= V; X : Pair with Atomic, Async_Readers, Async_Writers; function Max return Integer with Volatile_Function, Post => Max'Result /= 0; end Example_10;
package body Example_10 is function Max return Integer is P : constant Pair := X; Val1 : constant Natural := P.U; Val2 : constant Natural := P.V; begin return Natural'Max (Val1, Val2); end Max; end Example_10;

This code is correct. Values of P.U and P.V are provably different, and the postcondition is proved.