# How do you handle console IO and string manipulation in SPARK?
**URL:** https://forum.ada-lang.io/t/how-do-you-handle-console-io-and-string-manipulation-in-spark/4692
**Category:** General
**Tags:** spark, ada
**Created:** [August 29, 2026, 7:03am UTC](https://forum.ada-lang.io/t/how-do-you-handle-console-io-and-string-manipulation-in-spark/4692 "2026-08-29T07:03:06Z")
**Posts on this page:** 15
**Page:** 1
### Author:  [@ValorZard](https://forum.ada-lang.io/u/ValorZard)
#### Post date: [August 29, 2026, 7:03am UTC](https://forum.ada-lang.io/t/how-do-you-handle-console-io-and-string-manipulation-in-spark/4692/1 "2026-08-29T07:03:06Z")
Hey yall!
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?
---
### Author:  [@damaki](https://forum.ada-lang.io/u/damaki)
#### Post date: [August 29, 2026, 9:26am UTC](https://forum.ada-lang.io/t/how-do-you-handle-console-io-and-string-manipulation-in-spark/4692/2 "2026-08-29T09:26:01Z")
> [@ValorZard](#):
>
> Is there a way to print to console with Put\_Line in a multithreaded SPARK context?
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:
```ada
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;
```
> [@ValorZard](#):
>
> 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 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 `"&"`:
```ada
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:
```ada
function Concat (A, B : Unbounded_String) return Unbounded_String
is (A & B)
with Pre => Length (A) <= Natural'Last - Length (B);
```
---
### Author:  [@dmitry-kazakov](https://forum.ada-lang.io/u/dmitry-kazakov)
#### Post date: [August 29, 2026, 10:04am UTC](https://forum.ada-lang.io/t/how-do-you-handle-console-io-and-string-manipulation-in-spark/4692/3 "2026-08-29T10:04:59Z")
> [@damaki](#):
>
> 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
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.
---
### Author:  [@damaki](https://forum.ada-lang.io/u/damaki)
#### Post date: [August 29, 2026, 10:28am UTC](https://forum.ada-lang.io/t/how-do-you-handle-console-io-and-string-manipulation-in-spark/4692/4 "2026-08-29T10:28:12Z")
> [@dmitry-kazakov](#):
>
> Using potentially blocking operation during a protected action is a bounded error. Put\_Line is potentially blocking.
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`.
> [@dmitry-kazakov](#):
>
> 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.
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](https://docs.adacore.com/spark2014-docs/html/ug/en/source/concurrency.html#preventing-data-races).
---
### Author:  [@dmitry-kazakov](https://forum.ada-lang.io/u/dmitry-kazakov)
#### Post date: [August 29, 2026, 10:53am UTC](https://forum.ada-lang.io/t/how-do-you-handle-console-io-and-string-manipulation-in-spark/4692/5 "2026-08-29T10:53:10Z")
> [@damaki](#):
>
> What mutexes are you talking about here? Something like a `pthread_mutex`?
No, in Ada a mutex is typically implemented using a protected object, e.g. in [Simple Components](https://www.dmitry-kazakov.de/ada/components.htm#Mutexes). 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.
---
### Author:  [@damaki](https://forum.ada-lang.io/u/damaki)
#### Post date: [August 29, 2026, 11:52am UTC](https://forum.ada-lang.io/t/how-do-you-handle-console-io-and-string-manipulation-in-spark/4692/6 "2026-08-29T11:52:04Z")
> [@dmitry-kazakov](#):
>
> No, in Ada a mutex is typically implemented using a protected object, e.g. in [Simple Components](https://www.dmitry-kazakov.de/ada/components.htm#Mutexes). The difference is that it becomes two protected actions ( **Seize** and **Release** ) and the blocking call happens in between.
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.
---
### Author:  [@dmitry-kazakov](https://forum.ada-lang.io/u/dmitry-kazakov)
#### Post date: [August 29, 2026, 12:40pm UTC](https://forum.ada-lang.io/t/how-do-you-handle-console-io-and-string-manipulation-in-spark/4692/7 "2026-08-29T12:40:54Z")
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.
---
### Author:  [@damaki](https://forum.ada-lang.io/u/damaki)
#### Post date: [August 29, 2026, 1:09pm UTC](https://forum.ada-lang.io/t/how-do-you-handle-console-io-and-string-manipulation-in-spark/4692/8 "2026-08-29T13:09:39Z")
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.
---
### Author:  [@dmitry-kazakov](https://forum.ada-lang.io/u/dmitry-kazakov)
#### Post date: [August 29, 2026, 1:28pm UTC](https://forum.ada-lang.io/t/how-do-you-handle-console-io-and-string-manipulation-in-spark/4692/9 "2026-08-29T13:28:10Z")
The thing you need to prove is _Console\_Mutex.Is\_Owned_ in the precondition of _Write\_Console_.
---
### Author:  [@damaki](https://forum.ada-lang.io/u/damaki)
#### Post date: [August 29, 2026, 2:11pm UTC](https://forum.ada-lang.io/t/how-do-you-handle-console-io-and-string-manipulation-in-spark/4692/10 "2026-08-29T14:11:13Z")
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](https://docs.adacore.com/spark2014-docs/html/ug/en/source/concurrency.html#state-abstraction-and-concurrency)). 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)](https://docs.adacore.com/spark2014-docs/html/lrm/packages.html#external-state-variables-and-types)).
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 🙂
---
### Author:  [@dmitry-kazakov](https://forum.ada-lang.io/u/dmitry-kazakov)
#### Post date: [August 29, 2026, 2:43pm UTC](https://forum.ada-lang.io/t/how-do-you-handle-console-io-and-string-manipulation-in-spark/4692/11 "2026-08-29T14:43:10Z")
What about passing a mutex holder to `Write_Console`?
```ada
declare
Lock : Holder (Console_Mutex'Access);
begin
Write_Console (Lock, "I am under mutex");
end;
```
---
### Author:  [@damaki](https://forum.ada-lang.io/u/damaki)
#### Post date: [August 29, 2026, 3:14pm UTC](https://forum.ada-lang.io/t/how-do-you-handle-console-io-and-string-manipulation-in-spark/4692/12 "2026-08-29T15:14:40Z")
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.
---
### Author:  [@damaki](https://forum.ada-lang.io/u/damaki)
#### Post date: [August 29, 2026, 3:40pm UTC](https://forum.ada-lang.io/t/how-do-you-handle-console-io-and-string-manipulation-in-spark/4692/13 "2026-08-29T15:40:11Z")
> [@damaki](#):
>
> 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](https://github.com/damaki/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).
---
### Author:  [@ValorZard](https://forum.ada-lang.io/u/ValorZard)
#### Post date: [August 29, 2026, 4:40pm UTC](https://forum.ada-lang.io/t/how-do-you-handle-console-io-and-string-manipulation-in-spark/4692/14 "2026-08-29T16:40:22Z")
Oh this is very interesting!
My current goal is to make a SPARK proven io\_uring runtime in Ada (similar to [Seastar in C++](https://github.com/scylladb/seastar)) so this feels relevant!
---
### Author:  [@dmitry-kazakov](https://forum.ada-lang.io/u/dmitry-kazakov)
#### Post date: [August 29, 2026, 5:17pm UTC](https://forum.ada-lang.io/t/how-do-you-handle-console-io-and-string-manipulation-in-spark/4692/15 "2026-08-29T17:17:58Z")
> [@damaki](#):
>
> Unfortunately SPARK doesn’t support pointers to effectively volatile objects
But can do:
```ada
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