saeaadl / aadlv2.2

SAE AADL core language, version 2.2
1 stars 0 forks source link

Add Halt in event port to reserved thread ports #70

Closed brlarson closed 2 years ago

brlarson commented 2 years ago

Indication that Finalize_Entrypoint should be invoked caused by an event issued by a component other than the thread with the Halt in event port will complement other reserved ports, particularly Stop.

Suggested additions: 5.4 (6) Receiving an event on the reserved Halt in event port causes the thread to terminate normally.

5.4 (C1) remove the "and" before stop and append ", Halt must be in event port"

5.4 insert after (12) Every thread has reserved in event port named Halt. If this port is connected, an an event received on it, the Finalize_Entrypoint shall be called before terminating.

5.4.1 (27) c adequately defines the transition to performing thread finalize caused by invocation of Finalize_Entrypoint, so no changes to Figure 5 are needed.

"Halt" is an appropriate identifier for the ports because it leads to the thread halted state in Figure 5.

jjhugues commented 2 years ago

It is not clear to me if we want this to be an explicit port or not.

The standard has " A Finalize_Entrypoint (enter the state performing thread finalize in Figure 5) is executed when a thread is asked to terminate as part of a process unload or process stop."

But a process is not (per se) an active component. I always interpreted Finalize_Entrypoint to be executed implicitly by the runtime, not explicitly by a Send_Output from some other threads.

brlarson commented 2 years ago

BA allows multiple final states to model both normal and abnormal termination. A thread may choose to enter a final state on its own criteria, or be signaled by another component. Defining a reserved halt in event port allows the thread to make one or more state transitions to free resources, save persistent state, or other finalization activities in the context of a state machine. A reserved port identifier representing abnormal termination, without finalization, caused externally to the thread may also be useful.

jjhugues commented 2 years ago

Adding a halt port makes sense for some classes of system. However this triggers many more questions

Just to make sure we review the documents with the same elements: figure 5 mentions that thread finallization is called only in the case of stop(process/processor/etc). This is different from thread deactivation that is called when a thread exists a mode. In addition, dispatch protocols haven been defined under the strict hypothesis that a thread never ends, unless one of the two previous situations are met. In other words, no self termination, no termination requested by another thread.

Adding a specific halt event port would force a complete rewrite of this part. Also, this triggers many side effects. You mention freeing resources, but this does not account for connections as well.

The modeling pattern for this problem is to rely on modes, as suggested by the Ravenscar profile. If the mode is "final" (in that you cannot reach another mode), then you can claim more resources after the execution of the Deactivate_Entrypoint. Having a halt port seems too dangerous IMO

jjhugues commented 2 years ago

Discussed today during committee meeting: the resolution is to use modes and not a specific port