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:
Xis volatileXis also an output; outputXdepends on inputXXis only read
Volatile Variables and Volatile Types
Variables whose reads/writes cannot be optimized away
Identified through multiple aspects (or pragmas)
aspect
Volatilebut also aspect
Atomicand GNAT aspect
Volatile_Full_Accessall the above aspects can be set on type or object
Other aspects are useful on volatile variables
aspect
Addressto specify location in memoryaspect
Importto 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_Readersif variable may be read asynchronouslyAsync_Writersif variable may be written asynchronously
Effect of
Async_Readerson flow analysisEffect of
Async_Writerson flow analysis & proofalways 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_Readsif reading the variable has an effect on its valueEffective_Writesif 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
TrueWhen some aspects set, all others default to
False
Only half the possible combinations are legal
Async_Readersand/orAsync_Writersis setEffective_Reads = TrueforcesAsync_Writers = TrueEffective_Writes = TrueforcesAsync_Readers = Truesensor:
AW=Trueactuator:
AR=Trueinput port:
AW=True,ER=Trueoutput 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=Truemust appear alone on rhs of assigna 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=Trueis marked as volatile with aspectVolatile_Functioncalls 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
ExternalFlavors 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_Writershave no known value... but they have a known type!
type range, ex:
0 .. 360type predicate, ex:
0 .. 15 | 17 .. 42 | 43 .. 360
Variables without
Async_Writershave a known valueGNATprove 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.