I’ve been doing some more stuff with Ada and spark, and my goal has been to write programs that can be 100% audited with SPARK.
However one issue I run into is how to handle printing out text and getting text. When using the Jorvik profile, it turns out workers can’t print to the console without causing a data race.
Is there a way to print to console with Put_Line in a multithreaded SPARK context?
Additionally, are types like unbounded strings (or appending strings together to form messages) just completely forbidden in SPARK, or are there workarounds I just don’t know about yet?
You could define a protected object (PO) that wraps operations such as Ada.Text_IO.Put_Line, then ensure all your text IO goes through that protected object. The PO will ensure that only one thread has access at a time, which will satisfy SPARK’s race condition checks.
For example:
protected Protected_Text_IO is
procedure Put_Line (Item : String);
end Protected_Text_IO;
protected body Protected_Text_IO is
procedure Put_Line (Item : String) is
begin
Ada.Text_IO.Put_Line (Item);
end Put_Line;
end Protected_Text_IO;
You can use Unbounded_String in SPARK. GNAT’s implementation of Ada.Strings.Unbounded has SPARK contracts. What problems are you having with it?
If you’re hitting unproved checks when concatenating strings, you probably need to give more information to the prover to show that the combined length does not exceed Natural'Last.
For example, SPARK cannot prove the following function, because strings A and B could be any length (including Natural'Last), and SPARK cannot show that Length (A) + Length (B) <= Natural'Last which is required by the precondition of "&":
function Concat (A, B : Unbounded_String) return Unbounded_String
is (A & B);
However, if I add a precondition that constrains the lengths of A and B to avoid overflow, then SPARK can prove that the concatenation will not overflow the length:
function Concat (A, B : Unbounded_String) return Unbounded_String
is (A & B)
with Pre => Length (A) <= Natural'Last - Length (B);
Using potentially blocking operation during a protected action is a bounded error. Put_Line is potentially blocking.
AFAIK, GNAT specifically permits using Put_Line from protected actions, but it is compiler-specific and might depend on the target.
If you want interlocked output outside a protected action, use a mutex. Inside a protected actions use a ring buffer flushed by next call from outside the action.
Good point. I’m not sure if the potentially blocking aspect is modelled by SPARK for these operations, since the bodies are not visible in SPARK (they have SPARK_Mode => Off).
For native runtimes I don’t know if GNAT permits Put_Line from protected actions or not, but FYI for GNAT bareboard runtimes the implementation of Ada.Text_IO does not perform any potentially blocking operations (they write to something like a UART or semihosting directly).
A workaround to this (if potentially blocking calls in Ada.Text_IO are a problem) could be to hold a queue to hold messages in the protected object, then one dedicated task can read from this queue and call Ada.Text_IO.
What mutexes are you talking about here? Something like a pthread_mutex? If so, that would unfortunately not be compatible with SPARK. SPARK’s analysis currently only allows tasks to share synchronized objects (protected objects, atomic objects, or Suspension_Object) to prevent data races, as per Section 5.10.1.2 of the SPARK User Guide.
No, in Ada a mutex is typically implemented using a protected object, e.g. in Simple Components. The difference is that it becomes two protected actions (Seize and Release) and the blocking call happens in between.
Another model is a so-called monitor, using rendezvous with a dedicated task, but it is more heavyweight. Typically you would copy the buffer contents inside the entry and let the task do actual output asynchronously (which might require context switches). However, on a bare bones target it might become preferable if the physical I/O performed from that very task.
Thanks for clarifying. While this pattern is fine for plain Ada, it unfortunately is not compatible with the way SPARK proves absence of data races because the knowledge of which resource(s) a mutex guards and the fact that Grab gives excludes exclusive access are not modeled in contracts, so the proof tools have no knowledge of them and therefore cannot prove absence of data races.
You need higher-level contracts while mutex hidden inside the implementation. At some point, deep down, you always must give your word (axiomatize) instead of a proof. E.g. you cannot prove that pragma Atomic does what it claims, you rely on that axiom.
Having said that, I am not competent in SPARK to tell, but possibly there are ways to prove that ceritan calls occur only with the mutex taken.
I have a fair amount of experience with SPARK, including for multitasking programs in a bare-metal environment, and unfortunately I’m not aware of any way to express absence of data races to GNATprove using such a mutex pattern.
I agree that at some point you need to rely on assumptions, but I generally recommend avoiding assumptions when writing SPARK code (e.g. pragma Assume or SPARK_Mode => Off) whenever it is reasonably practicable to do so, as it is easy to make mistakes that invalidate other proofs.
In many cases, there are other ways to design the code to write it in a form that is more amenable for formal verification without resorting to assumptions. In the OP’s case, using a protected object with a dedicated I/O task would be the easiest pattern to prove absence of data races for Ada.Text_IO in SPARK.
It does look like that at first glance, but unfortunately the devil is often in the details
Console_Mutex is a protected object, which SPARK treats as effectively volatile meaning that its value as seen from a given task may change at any time due to some other task accessing the protected object (See SPARK UG § 5.10.5). This volatility means that from the provers’ point of view, querying the protected object (Is_Owned in this case) may return a different value each time it is called and therefore it is not possible to prove that it will be True at the precondition of Write_Console.
SPARK prohibits the use of effectively volatile calls or objects in contracts for exactly this kind of reason (SPARK RM 7.1.3 (9)).
Even if you could prove Console_Mutex.Is_Owned in the precondition of Write_Console, there are also several other pieces of implicit information that are not formally specified in contracts/predicates (so the provers know nothing about them) that would be necessary to prove absence of data races:
the fact that Is_Owned returns True says nothing about giving exclusive access to a resource.
there is nothing stating which object are protected by the mutex and are therefore safe to access when Is_Owned is True.
Is_Owned = True says nothing about which task has ownership of the mutex. In fact, there’s no concept of ownership expressed by the mutex.
So yeah, unfortunately when trying to formally verify things we need to make the necessary information explicit to the provers in a format they understand (types, predicates, contracts, etc), and not everything can expressed in the way that seems obvious at first glance.
There may be ways to design a mutex that would be more amenable to formal verification with SPARK, perhaps by taking advantage of access types and SPARK’s ownership semantics to return an exclusive borrow of some data, but I’ll leave that as an exercise for the reader
Unfortunately SPARK doesn’t support pointers to effectively volatile objects (including protected or atomic objects), so Console_Mutex'Access won’t be SPARK-compatible.
It might be possible going the other way, though, where Lock could move a handle/holder that holds a pointer to the data itself, then a traversal function on the holder like function Get_Data (H : Holder) return not null access Data_Type could return a borrow to the data. When you’re done with it, you can call Unlock to pass the holder back to the PO.
The only other challenges I can foresee is proving that the holder can only be passed back to the correct mutex (i.e. that it can’t be obtained from one mutex then given back to another), and proving that the mutex’s internal holder is null when Unlock is called with a valid handle.
I actually faced a very similar problem when I wrote LibSAP (a zero-copy inter-task message passing library in SPARK), where I have a fixed-size pool of objects used for message transactions. Handles were used to hold a pointer to the transaction data, and at the end of a transaction ownership of the transaction data is moved from the handle back to the pool. It’s there I had the problem; with proving that the pool didn’t already have a non-null pointer in that slot.
In the end, I had to resort to using a pragma Assume to tell the provers that the pool’s pointer would always be null at that point, and I used several design techniques to ensure that this assumption cannot be violated:
each Transaction_Data object is given a unique transaction ID (TID). The uniqueness of the TID is guaranteed by:
the Transaction_Data type is an incomplete type in the package spec and completed in the body, so only the only place an object of type Transaction_Data can be allocated is in the package body. This prevents other packages from allocating an object and trying to return it back to the pool.
the only place where Transaction_Data objects are allocated in the package body is once during elaboration, where it allocates exactly one object for each possible TID.
the TID is an immutable discriminant of the Transaction_Data type, so it cannot change after initialization;
predicates and contracts ensure that each Transaction_Data object can only be stored in the slot corresponding to its TID.
SPARK’s ownership rules ensure that there is only ever one owner of the pointer to a Transaction_Data object at a time.
So since there is only ever one instance per TID, and SPARK’s ownership rules guarantee that there is only ever one pointer to that TID at a time, if the handle currently owns a pointer with that TID, then the pool’s pointer must be null.
The only way to violate this assumption (that I could think of) is by very intentionally bypassing SPARK by either:
declaring a child package to get access to the private definition of the handle types, to therefore get access to the handle’s internal pointer to create copies. Though SPARK’s ownership rules would detect and prevent copies of the pointer from being made.
using hacks like memory overlays or unchecked conversions to get access to things that are normally prevented by language rules.
As an extra safety net I wrote an explicit run-time check immediately after the pragma Assume to detect if the assumption is ever violated. Even if the assumption was violated, it would still be memory-safe (the worst case would be a resource leak).
procedure Write_Console (Text : String) is
begin
Lock.Seize;
begin
Ada.Text_IO.Put_Line (Text);
Lock.Release;
exception
when others =>
Lock.Release;
raise;
end;
end Write_Console;
And ensure that Ada.Text_IO is not used in any other package.
BTW, in what sense the term “data race” is used. Clearly writing console has race condition. The only question is granulation of the atomic item. E.g. character vs line vs message vs exchange etc
