Capstone: Concurrent Sensor Monitoring System
Integrate advanced Ada: a generic statistics package with contracts, a protected bounded queue with barriers, producer task types with discriminants, a consumer task, subtypes with ranges, deterministic simulated measurements, and precondition-guarded operations — then review the design choices.
The capstone ties together generics, contracts, tasking and protected objects. Three producer tasks simulate sensors, pushing readings into a protected bounded queue; a consumer aggregates statistics per sensor with a generic, contract-checked accumulator. Although the tasks interleave nondeterministically, the results are deterministic because every reading is processed exactly once.
Architecture
Sensors declares the domain types (Sensor_Id range 1 .. 3, Celsius range -50 .. 150, Reading), a generic Statistics package (for any signed integer Sample type) with Post on Add and Pre on Mean/Max, and a protected type Reading_Queue with an 8-slot modular ring buffer whose entries block producers when full and the consumer when empty. The main procedure instantiates Statistics for Celsius, starts three Producer (Id) tasks inside a block (joining them), waits for the consumer, and prints a table. Measure is a formula so the program is reproducible without hardware.
• Generic + contracts: reusable, self-checking statistics. • Protected ring buffer: synchronization via barriers. • Task types with discriminants; block = join. • Deterministic data despite nondeterministic scheduling.
Code Examples
Each sensor produces 20 readings; the consumer processes all 60. Only sensor 3 reaches ≥ 55 °C (twice). Calling Mean on an empty accumulator violates its precondition. Output: Sensor Count Mean Max 1 20 29 36 2 20 39 46 3 20 49 56 Readings >= 55 C: 2 Mean of an empty accumulator rejected by its precondition
-- file: sensors.ads
-- Capstone: a concurrent, contract-checked sensor monitoring system
package Sensors is
type Sensor_Id is range 1 .. 3;
subtype Celsius is Integer range -50 .. 150;
type Reading is record
Sensor : Sensor_Id;
Value : Celsius;
Seq : Positive;
end record;
-- Generic statistics over any numeric sample type
generic
type Sample is range <>;
package Statistics is
type Accumulator is private;
procedure Add (A : in out Accumulator; X : Sample)
with Post => Count (A) = Count (A'Old) + 1;
function Count (A : Accumulator) return Natural;
function Mean (A : Accumulator) return Sample
with Pre => Count (A) > 0;
function Max (A : Accumulator) return Sample
with Pre => Count (A) > 0;
private
type Accumulator is record
N : Natural := 0;
Sum : Long_Long_Integer := 0;
High : Sample := Sample'First;
end record;
end Statistics;
-- Thread-safe bounded queue between producers and the consumer
type Slot_Index is mod 8;
type Slots is array (Slot_Index) of Reading;
protected type Reading_Queue is
entry Put (R : R
…Design Review
Why a protected object rather than a rendezvous server? It is lighter, Ravenscar-compatible (with one entry per object in stricter profiles, you would split Put and Get into two objects or use Suspension_Objects), and barriers express the buffer conditions declaratively. Why a generic? The same statistics code serves Celsius, pressure or any other integer quantity. Improvements: add a Type_Invariant on Accumulator, use Ada.Real_Time with delay until for periodic sampling, log consumer exceptions with Exception_Information, prove the queue and statistics in SPARK, and replace the busy wait on Consumer'Terminated by declaring the consumer inside a block.
• Protected objects over rendezvous for data exchange. • Generics for reuse across quantities. • Next steps: invariants, periodic tasks, SPARK proof, structured joins.
-- producers printing their own readings directly -- aggregate in one place and print after joining
Printing from several tasks gives interleaved, nondeterministic output.
Alarms:= Alarms + 1; -- from several producer tasks -- count in the single consumer (as here) or in a protected object
Only one task updates Alarms, so there is no race.
function Mean (A: Accumulator) return Sample; -- divides by zero when empty function Mean (A: Accumulator) return Sample with Pre => Count (A) > 0;
The precondition documents and checks the requirement.
Why is the capstone's output deterministic despite concurrency? A. Tasks run sequentially B. Every reading is processed exactly once and aggregation is order-independent C. Random seed D. It isn't
What blocks a producer when the queue is full? A. A busy loop B. The Put entry's barrier Count < Slots'Length C. An exception D. delay
How are the three producers joined? A. join() B. They are declared in a block, which waits for them to terminate C. abort D. Semaphores
What does Statistics being generic over 'type Sample is range <>' allow? A. Any floating type B. Any signed integer type C. Only Integer D. Strings Trace the capstone output.
Real output: Sensor Count Mean Max 1 20 29 36 2 20 39 46 3 20 49 56 Readings >= 55 C: 2 Mean of an empty accumulator rejected by its precondition
-- file: sensors.ads
-- Capstone: a concurrent, contract-checked sensor monitoring system
package Sensors is
type Sensor_Id is range 1 .. 3;
subtype Celsius is Integer range -50 .. 150;
type Reading is record
Sensor : Sensor_Id;
Value : Celsius;
Seq : Positive;
end record;
-- Generic statistics over any numeric sample type
generic
type Sample is range <>;
package Statistics is
type Accumulator is private;
procedure Add (A : in out Accumulator; X : Sample)
with Post => Count (A) = Count (A'Old) + 1;
function Count (A : Accumulator) return Natural;
function Mean (A : Accumulator) return Sample
with Pre => Count (A) > 0;
function Max (A : Accumulator) return Sample
with Pre => Count (A) > 0;
private
type Accumulator is record
N : Natural := 0;
Sum : Long_Long_Integer := 0;
High : Sample := Sample'First;
end record;
end Statistics;
-- Thread-safe bounded queue between producers and the consumer
type Slot_Index is mod 8;
type Slots is array (Slot_Index) of Reading;
protected type Reading_Queue is
entry Put (R : R
…