I’m working on a system in SPARK and am confused by a warning SPARK is giving about data races.
I’m working on a message passing system that manages several endpoints. There are multiple types of messages. Each message is a record with a Message_Type component specifying the type of the message. To use the system, endpoints use a register procedure and declare what message types they’re allowed to receive.
The system tracks what types of messages can be received by each endpoint in an abstract package state Metadata with Ghost belonging to the message system package. The Send_Message procedure then has preconditions that check with the message system to verify that the receiving endpoint has declared it can receive the type of message being sent.
All the endpoints are initialized at the start of the program by a single thread. Later in the program they’re used by different threads. These later threads will never need to alter Metadata. They take it as a Proof_In global variable.
SPARK is saying that there is a data race possible because the multiple threads are using the Metadata state.
cubedos-time_server-messages.adb:85:09: high: possible data race when accessing variable “message_manager.mailbox_metadata”[#2]
cubedos-time_server-messages.adb:85:09: high: task “cubedos.time_server.messages.send_tick_messages” accesses “message_manager.mailbox_metadata”[#3]
cubedos-time_server-messages.adb:85:09: high: task “cubedos.time_server.messages.message_loop” accesses “message_manager.mailbox_metadata”[#4]
How is this possible? If Metadata is Ghost, shouldn’t it never actually be evaluated at runtime?
Suppose that Metadata wasn’t Ghost. Is there a way I can communicate to SPARK that Metadata should be immutable after all the endpoints are initialized?
SPARK has the Constant_After_Elaboration aspect for this. It does mean that the value has to be set by the time the elaboration of the package ends. If you can’t use that, you could make it a protected object.
The issue is that GNATprove does not know how your threads are scheduled. For what it knows, the writes and reads to Metadata could all occur at the same time. You could make it Constant_After_Elaboration as indicated above, but that means you need the elaboration code to initialize the value instead of a thread. You could use a protected object, but I don’t know if that’s feasible in your code.
Another way is to hide the fact that this data is mutable, by hiding it under public setters/getters, where the getters would be annotated with Global => null so that they always return the same value. The body will need to be in SPARK_Mode => Off as you will actually read global data, but you can review that Ada code to ensure that the assumption of only calling getters after the last write has taken effect is true.
By the way, the variable being Ghost or not does not change anything. While ghost code is not activated typically in production code, it can be executed, and it has the same semantics as regular code. So it can fail similarly, and suffer from race conditions too.
I’ve decided to hide the mutability of the metadata from SPARK. I’ve encountered another problem though. I created getters for the data which read from the protected object. Their specification has Global => null and Depends => (Func'Result => null) and the body has SPARK_Mode => Off.
When I use the function in the same package as it is declared, the fact that it is a blocking subprogram is ignored as expected. A problem is that SPARK assumes that the function may be blocking. Is it possible that I can hide things from SPARK more selectively? Could I specify somehow that the function isn’t blocking?