[RFC] Generalized finalization

[raph-amiard]

This work is based upon the work of @Roldak on Lightweight finalization https://github.com/AdaCore/ada-spark-rfcs/pull/65.

The idea the same, eg. to provide a way to have finalization in Ada that is:

1. Faster - or more precisely easier for a compiler to provide a fast implementation of
2. Usable in restricted contexts (less complex to implement/no or little runtime support needed)
3. Usable without tagged types

The additions of this version of the RFC on top of what Romain did earlier is:

• Investigate more precisely what in the current definition of controlled types is a limit to a fast implementation (precisely, behavior in case of raise in a finalizer, see ARM 7.6.1)
• Clearly identify the only other area that has a performance implication (finalization of heap allocated objects). At this stage we're pretty confident that both of those items are it.
• Make the model a superset of existing Ada controlled types, and re-specify Ada.Finalization.Controlled in terms of the current model.

This feature is made of two RFCs:

• Generalized finalization RFC - the main one
• No_Raise aspect

[!WARNING] This is not an RFC about object orientation. This is a redefinition of the underlying finalization model, with some provisions to make it usable out of the box. In particular, it is expected that prototyping of destructors in https://github.com/AdaCore/ada-spark-rfcs/pull/106 should be done on top of this.

[yannickmoy]

A few thoughts on No_Raise:

• why make it raise Assertion_Error at runtime in case the subprogram raises an exception? It would look more regular to me to raise Program_Error in that case, like for returning from a No_Return procedure or propagating an exception from a Finalize procedure in a controlled object (see Ada RM 7.6.1(14-20)). Also, I find it bizarre that it can be opted out with a check category.
• another option is to make it erroneous to raise an exception from a No_Raise subprogram, and do nothing special in GNAT: an exception is raised, which may or not terminate immediately the execution depending on the runtime.
• in SPARK, No_Raise would be equivalent to the contract Exceptional_Cases => (others => False) which specifies that no exceptions are allowed to be raised by the subprogram. Still, it makes sense to have a shorthand for this useful specification.

About generalized finalization, it looks a bit heavy to me to introduce 6 new aspects for that functionality. Why not do like for aspect Iterable, and group these names under a single aspect Finalizable? The name Exceptions_In_Finalize would be better named Exceptions_In_Finalization for consistency with Legacy_Heap_Finalization.

For types that allow exceptions in finalization, I suppose Finalize should not have the aspect No_Raise, which is not currently stated in the RFC.

The RFC does not say which types can be finalizable. I suspect it only makes sense for objects passed by reference? Thus, we could decide that this aspect makes the type a by-reference type. And also forbid it on by-copy types.

The "unresolved questions" of the RFC states that "a Finalize raising an exception will make the program abort by default` which is not what the RFC currently says.

[clairedross]

Note that in SPARK, Exceptional_Cases => (others => False) is the default.

[raph-amiard]

About generalized finalization, it looks a bit heavy to me to introduce 6 new aspects for that functionality. Why not do like for aspect Iterable, and group these names under a single aspect Finalizable? The name Exceptions_In_Finalize would be better named Exceptions_In_Finalization for consistency with Legacy_Heap_Finalization.

I agree, good suggestion, I'll amend the RFC to reflect that

For types that allow exceptions in finalization, I suppose Finalize should not have the aspect No_Raise, which is not currently stated in the RFC.

I don't think that's necessary, IMO Finalize, or any procedure for that matter, can have the No_Raise aspect without it being a problem.

The RFC does not say which types can be finalizable. I suspect it only makes sense for objects passed by reference? Thus, we could decide that this aspect makes the type a by-reference type. And also forbid it on by-copy types.

Hmm, it's true that falling out of the fact that they're tagged, every finalizable type so far in Ada is by-reference. I do think however that Rust and C++ allow by-copy finalizable types. Let me think on this.

The "unresolved questions" of the RFC states that "a Finalize raising an exception will make the program abort by default` which is not what the RFC currently says.

Good catch. That was another possible alternative (corresponding to what C++ does).

why make it raise Assertion Error at runtime in case the subprogram raises an exception

@sabaird Sent me similar comments about Assertion Error vs Program Error, Ill try to explain the rationale of the choice I made here.

First, for a bit of context:

• In C++ a destructor should not raise an exception either. Starting from C++11, all destructors are implicitly declared as noexcept. This means that if a destructor raises an exception, std::terminate will be called. An important thing to know though is that historically code that uses exceptions in C++ is very rare, and basic language operations rarely raise exceptions. This might explain why it seems OK in C++ world. IMO it's too drastic & dangerous in Ada.
• In Rust, the situation is a bit more complex. There are no exceptions in Rust, but there is panic, and 'panic' can use unwinding in some configurations, and can be caught. Depending on the configuration, panic drop implementations could panic. And some people think that in some configs, for resilient programming, being able to catch a panic, even from a drop, is a good idea. See the discussion here: https://github.com/rust-lang/lang-team/issues/97

What I get out of this and the Rust discussion is that

1. In dev and testing you definitely want an exception raised in your finalizer to be a fatal and not be spuriously caught by an exception handier that is too wide. In that regard, Program_Error probably fits the bill as well, but you don't want, at least by default, the behavior of just propagating exceptions.

To further this point, some libraries in Ada (like LAL but not only LAL) use the pattern of exceptions being regular errors that can happen (Property_Error in LAL for example). If such an error was raised in a destructor, you'd want to catch that in order to refactor the code to not call this code in the destructor if possible, or to catch the possible exception, in order to avoid resources leaks.

2. However, in many production scenarios where you want to have resilient applications (The Rust thread cites web server. With the LAL example above, IDEs come to mind. In Ada in general, early abort scenarios can make us think of the Arianne scenario) having such an error crash your program is a bad idea, because it's too drastic. In those cases you want to continue even though you had an exception in a finalizer and might risk leaking some resources.

So, this is the context for the design in the RFC. The exact kind of the exception doesn't matter much to me, but it's very important IMO to make this "crash early" behavior alterable for production builds in an easy fashion, and assertions behave like this in Ada, which did seem like a good fit.

Also, if you conceptualize No Except as a contract (and it is what it is IMO) then I really don't see the problem having subprograms who breach the contract raise an 'Assertion_Error`.

In light of the above:

another option is to make it erroneous to raise an exception from a No_Raise subprogram, and do nothing special in GNAT: an exception is raised, which may or not terminate immediately the execution depending on the runtime.

I think this is last resort and should be avoided if we can. Having a well documented behavior is important IMO for the reasons described above.

This is also why, after consideration, I put the C++ "terminate the program" option off the table.

[yannickmoy]

I don't think that's necessary, IMO Finalize, or any procedure for that matter, can have the No_Raise aspect without it being a problem.

I meant that in that case, Finalize should not be forced to have the No_Raise aspect, since in fact we allow it to raise an exception.

Hmm, it's true that falling out of the fact that they're tagged, every finalizable type so far in Ada is by-reference. I do think however that Rust and C++ allow by-copy finalizable types. Let me think on this.

The issue is that, for a by-copy type, the insertion of the calls to Initialize/Adjust/Finalize will depend on whether the compiler chooses the type to be by-copy or by-reference, which makes it more difficult to analyze (for analysis tools, which must have the same information) and to review (for human reviewers).

Thanks for the rationle on your choice of strategy for when an exception is raised from a Finalize procedure. I think however that raising Program_Error makes more sense here than Assertion_Error. There should be no assertion kind to change the behavior. This seems to fit your rationale as well, because Program_Error is an exception, that you can detect in dev/debug and catch in production code.

[raph-amiard]

After some live discussion with @yannickmoy, we can agree on Constraint_Error for the kind of the exception, and No_Raise_Check for the check category. @swbaird What do you think ?

[sttaft]

Program_Error still seems more natural to me. Constraint_Error generally implies there is some numeric range that is being violated, or a pointer is null. Raising an exception when none is expected seems very close to the return from a non-returning subprogram, and hence Program_Error.

[raph-amiard]

Ok @sttaft sounds good to me. What do you think about making this subject to a check category ?

[sttaft]

Ok @sttaft sounds good to me. What do you think about making this subject to a check category ?

For sure.  We try to make all checks subject to some check category.  The existing "Program_Error_Check" is already available as a fallback.  You had suggested a new Check category, which is fine, though I would call it "Raise_Check" rather than "No_Raise_Check", as we generally don't start Check names with "No" (whereas Restriction names use "No..." commonly).  For example, the check name "Overflow_Check" is associated with checking that there are no overflows. -Tuck

[raph-amiard]

Sounds great, thanks Tuck :+1:

[raph-amiard]

I pushed an update taking into account all the comments.

In particular:

• Regroup them all under one top-level aspect, like Iterable
• Unify the two configuration aspects into one
• Specify the behavior in terms of permission for the compiler
• Use Program_Error rt. Assertion_Error in the specification of No_Raise
• Enforce that this can only be specified on record types or private view of record types
• Correct the definition of Controlled (procedures are null not abstract)
• Document an unresolved question about finalized components with a different model than their enclosing record
• Document the future possibility of having a configuration pragma to set the default for Relaxed_Finalization to True for the controlled object root types.

[Roldak]

@raph-amiard I removed the TODO for the SPARk team as Claire confirmed this was the default, and Yannick mentioned it could be a useful shortcut to explicitly state the default.

Also I did the renaming of the category from No_Raise_Checks to Raise_Check as you seemed to agree with Tuck's message.

[yannickmoy]

minor comment: type U is record; in the first example is not correct Ada, it should be type U is null record;

[yannickmoy]

I think there is a typo when you say:

Finalize is only called when an object is implicitly deallocated. As a consequence, no-runtime support is needed for the implicit case

I think here you want to say that Finalize is only called for heap-allocated objects when the object is explicitly deallocated by calling an instance of Unchecked_Deallocation, or before it is assigned a new value, but not when exiting the scope of the corresponding access type. Is it what you had in mind?

[raph-amiard]

Thanks @Roldak and @yannickmoy and @sttaft , and everyone else who contributed. I think we're getting there