search

nim-lang / RFCs

A repository for your Nim proposals.
136 stars 23 forks source link

Introduce safety modes #180

Closed FedericoCeratto closed 4 years ago

FedericoCeratto commented 4 years ago

For some classes of applications safety, security and the ability to recover from exceptions and bugs are important. Nim could implement a safety option that:

Related:

Araq commented 4 years ago

Big -1 from me, we don't need more compiler and runtime modes, we need fewer. And let's also not conflate everything together, most experimental language features are about syntactic sugar and have no security impact.

mratsim commented 4 years ago

I'm not sure what kind of safety concerns you want to address but where safety is critical (aerospace, train scheduling systems, ...) what is required is completely different:

See the guarantees levels Spark Pro offer: https://www.adacore.com/sparkpro image

For me the biggest safety feature that we could bring is a spec extension (maybe similar to Crystal's) and have that compile to a formal verification language like Spin or TLA+ (tuto) and being able to check Nim code against the spec. Or we forge the spec extension and directly compile a restricted subset of Nim/stdlib to those languages.

This goes way beyond runtime checks or a borrow checker. This is similar to having a blueprint in civil or mechanical engineering, plan and verify the soundness of the design and then starting to build. This is not a replacement to runtime checks or Memory/Thread/AddressSanitizer by the way.

As an example, for Weave I was hunting several deadlocks and livelocks on my backoff mechanism (to put idle threads to sleep) and after spending a weekend dabbling into TLA+ I implemented my protocol, solved the logical and concurrency bugs (one did not exist with 2 threads, and was too rare with 8+ threads). Furthermore it allowed me to unravel a bug in glibc and musl condition variables where signaling them could be ignored, deadlocking the application. See https://github.com/mratsim/weave/issues/56.

While I don't expect Nim to be run on planes or space shuttles anytime soon:

Side-notes

Other references:

Araq commented 4 years ago

And also for the Nim language to not produce spurious ThreadSanitizer and AddressSanitizer warnings so that debugging low-level code is made easier.

At least that's addressed by --gc:arc.

Araq commented 4 years ago

I'm working on --panics:on/off (default is "off") that finally settles this cause. If panics are turned on you get the speed benefits of an optimizer that can assume that not everything can raise. If they are turned off, you can catch Defects just like today. For backwards compatibility --panics:off is the default.

timotheecour commented 4 years ago

when defined(safety):

s/safety/nimSafety/, new defined symbols need to be prefixed by package name (related: https://github.com/nim-lang/RFCs/issues/181)

arnetheduck commented 4 years ago

Does this mean we'll get an effect to track panics as well? I mean, so that we can statically prove that no panics happen in a piece of code?

timotheecour commented 4 years ago

Seems needed to implement araqs's sfalwaysreturn in his PR...

Araq commented 4 years ago

Does this mean we'll get an effect to track panics as well? I mean, so that we can statically prove that no panics happen in a piece of code?

Probably yes, but I have no final design for it.

timotheecour commented 4 years ago

proposal

these already have a meaning and should keep their meaning:

raises: []. # cannot raise a CatchableError (but could raise a Defect)
raises: [OsError]. # can only raise a OsError amongst the Catchable ones (but could raise a Defect)

so we introduce a new pragma:

exceptions: []. # cannot raise any Exception (so can't raise any Defect either)
exceptions: [OsError]. # can only raise a OsError (and no Defect)
exceptions: [AssertionError]. # can only raise a AssertionError (and no other Defect, unless subclass of AssertionError of course)
exceptions: [AssertionError, IndexError]. # obvious meaning
exceptions: [Defect]. # obvious meaning
exceptions: [Exception]. # obvious meaning
arnetheduck commented 4 years ago

@timotheecour: raises: [] means "no Defect exceptions" presently - only some defects are actually tracked though, so it's a bit random: https://github.com/nim-lang/Nim/issues/12862

after the PR by @Araq , there now seem to be 4 categories of errors to consider: Exception ("unknown, could be anything but you shouldn't really use this"), CatchableError ("you should catch these"), Defect ("you did something wrong with the API, you should maybe catch these") and panic/fatal ("you did something wrong with the API, and that API was part of the system library") - it would mean that some, but not all, of the things that are currently tracked by raises Defect will no longer cause that effect, so to detect them, we'd need something else.

Since the new proposed implementation depends on a compiler flag it means that if you're using a library that was written for one setting of the flag, and you're using raises, you can't mix that library with a library that was written for the other setting of the flag - on small projects that don't use raises this doesn't matter of course (which is most existing code, I guess - the low penetration of that particular feature is a signal perhaps?)

Araq commented 4 years ago

Why not simply .defects: [], .defects: [IndexError]?

timotheecour commented 4 years ago

there now seem to be 4 categories of errors to consider

no, it's simpler than what you describe;

Why not simply .defects: [], .defects: [IndexError]?

i thought about that too, but exceptions unifies it under 1 base class, exactly matching the Exception hierarchy This results in simpler (or equal) declarations in all cases:

exceptions: [] # same as your defects: [] raises:[]
exceptions: [IndexError] # same as your defects: [IndexError] raises:[]
exceptions: [OsError] # same as your defects: [] raises:[OsError]
raises: [OsError] # same as your raises:[OsError] # this could raise any defect, as well as OsError
raises: [] # same as your raises:[] # this could raise any defect, but no Catchable

note

everything is (obviously) expressible in terms of exceptions only, eg:

exceptions: [Foo], raises: [Bar] can be expressible as: exceptions: [Foo, Bar]
raises: [Bar] can be expressible as: exceptions: [Defect, Bar]

so raises is only for convenience of not having to specify Defect

Araq commented 4 years ago

everything is derived by the exception hierarchy

That's not true. (We could make it true though.) There is sysFatal (about to be renamed and exposed as panic) and --panics:on/off deals with panic whereas .raises is only concerned about the raise statement. But maybe keeping it tied to the exception hierarchy is the better idea. At least then there is only raise IndexError and not also raise IndexError vs panic IndexError.

timotheecour commented 4 years ago

ya, having a separate panic IndexError doesn't serve any useful purpose; tying to hierarchy makes sense

arnetheduck commented 4 years ago

But maybe keeping it tied to the exception hierarchy

this is very confusing in practice - the same constructs (try/catch and raises) being used for both "severities" of errors is difficult to educate around - it's "kind of" the same thing at that point - just another error, and deciding between the two when designing a library becomes very subjective - there's no clear boundary.

the consequence of having a global compiler flag for it is that you get completely different effects propagated through the code base making it impossible to mix panic:on and panic:off code - for example, it would be very hard to annotate the standard library itself with correct "raises" for both modes - this is a very real problem: almost everywhere where resources are managed in the standard library, there are leaks and errors because the code is not exception safe - these annotations should really be an explicit part of the standard library, because if you raise a new exception suddenly, that's a breaking API change.

timotheecour commented 4 years ago

but effect system tracks this so it only affects fwd decls

Araq commented 4 years ago

the consequence of having a global compiler flag for it is that you get completely different effects propagated through the code base making it impossible to mix panic:on and panic:off code

Why would you do that though... Just leave it turned off, isn't that what happened already? I introduced turning them on via --exceptions:goto (--gc:arc implies --exceptions:goto) and got so much backslash that I had to revert it.

timotheecour commented 4 years ago

IMO:

But other than that your application should usually not rely on Defect's being catchable as it should indicate a bug.

Araq commented 4 years ago

this is very confusing in practice - the same constructs (try/catch and raises) being used for both "severities" of errors is difficult to educate around - it's "kind of" the same thing at that point - just another error, and deciding between the two when designing a library becomes very subjective - there's no clear boundary.

Here is the problem: Let's assume that a panic Error is not the same as a raise Error. For raise you can use try except to catch it. For panic you need do use a recover errorHandler. Let's further assume that you really want to handle the panic and it must bubble up the call stack. What are you gonna do? So you write a raise statement in your errorHandler, you turn a panic into an exception. The optimizer must assume that every function call can fail. The programmer is also better off assuming this and to code appropriately, so nothing really was gained by Nim's exception tracking. IMHO.

zah commented 4 years ago

If we want to be able to have guarantees for panic-free (defect-free) code, then the current tracking of Defect already solves this. There are just issues that need to be resolved.

It's true that there are "educational" problems when it comes to the distinction between errors and defects, but I believe these problems will be present with any of the alternative proposals. Nim has few inappropriate defaults that exacerbate the problem:

1) Uneducated people tend to inherit from Exception. Nobody should do this, because it creates a third category of Errors. It's no longer possible to use the following pattern in the code:

prof foo() {.raises: [Defect, MyRecoverableError, OtherRecoverableError]`.}

Instead, you end up with procs that must be annotated with raises: [Exception] (see point 3 for more of this).

2) Uneducated people tend to write try: ..., except: .... This is currently bad, because it handles all defects. The default here should be CatchableError.

3) Uneducated people don't annotate their proc types and the default effect is set to raises: [Exception]. This is bad because it leads to libraries where the computed effect on all functions is raises: [Exception]. Such libraries are unusable in code that wants to use exception tracking. The language could be brave and set the default to raises: [Defect].

The two compilation modes (panics:on/off) are less of an issue in my opinion, because non-testing code should not discriminate between different types of defects by definition (defects are failures that are not anticipated in the normal operation of the program). Adding or removing defects to an API is a breaking change only when you are going from "no defects" to "some defects" and vice versa.

Araq commented 4 years ago

There is now a warning for (1) in Nim devel. Will do (2)-(3) for the upcoming release.

Edit: 2-3 are still to be done after 1.2.

alehander92 commented 4 years ago

Whenever one says Uneducated people tend to do x bad simple pattern, he should try to think of a way to make that simple pattern a compiler warning/error (or a linter one): there is no other good way to educate people (focus on simple to detect/explain)

Araq commented 4 years ago

Uneducated people don't annotate their proc types and the default effect is set to raises: [Exception]. This is bad because it leads to libraries where the computed effect on all functions is raises: [Exception]. Such libraries are unusable in code that wants to use exception tracking. The language could be brave and set the default to raises: [Defect].

That's what Java did, the most important problem is that when your library uses callbacks (in Java's case: interfaces), you as the library author do not know if the callback can raise something or not.

alehander92 commented 4 years ago

why not "generic" effects? function a raises exactly when arg callback b raises => proc a(b: proc: void {.raises: R.}): {.raises: R.} .. ? i guess too non-obvious api

Araq commented 4 years ago

The callback handler can also be inside an object, have fun with the complexities in the type system. ;-)

mratsim commented 4 years ago

This is bad because it leads to libraries where the computed effect on all functions is raises: [Exception]. Such libraries are unusable in code that wants to use exception tracking. The language could be brave and set the default to raises: [Defect]

There are seldom cases where it makes sense for a library to use exceptions instead of using errors or result/either. In my experience that's for libraries where consumers are not software engineers but domain experts like in:

For most other cases (IO, streams, networking, serialization, ...), it makes more sense to use errors at the low-level and let/force consumer applications (not libraries) deal with the error.

This makes the error model part of the API (the raises: [MyNewException] is an alternative but in practice no one pushed it far enough to show it worked), this makes it easier to provide libraries to consume from other language, this avoids the mistake of Python of using exceptions for all control flow and only coding/testing for the happy path (i.e. all files are found, network connection is never lost, and there is always disk space).

alehander92 commented 4 years ago

@Araq well .. you can annotate that if you really want :P :)

Araq commented 4 years ago

why not "generic" effects? function a raises exactly when arg callback b raises => proc a(b: proc: void {.raises: R.}): {.raises: R.} .. ? i guess too non-obvious api

Actually we have a variation of this rule in the effect tracking. It helps a little but also was complex to implement and I doubt many people understand it. ;-)

zah commented 4 years ago

Judging from the responses, I'm not sure my point about proc types was understood well, so I'll clarify.

Consider a library that uses a function pointer internally. For example, it may provide a user-hook or a callback for a certain operation. The library authors are likely to write their code like this:

type
  ClickHandler = proc (e: MouseEvent): bool

proc onClick(node: GuiElement, handler: ClickHandler) =
  node.clickHandler = handler

What happens next is that clickHandler is going to be called internally somewhere in the library. Since its effect is raises: [Exception] this infects every function that may end up calling it. For a sufficiently complicated library, all functions might be infected (for example, asyncdispatch fits that description).

If the language states that unannotated procs can raise only defects, a whole lot of usages of callbacks will stop compiling and the users will have to think about either handling the exceptions or providing a correct annotation for the callback.

arnetheduck commented 4 years ago

why not "generic" effects?

... or just make exceptions a strict requirement of the function signature - this is already kind of possible (but there are a few language features missing to make this truly convenient): func f[X, E: ref Exception](): Result[X, E] - in fact, I'd love to have this capability not just for callbacks but also for templates:

https://github.com/status-im/nim-stew/blob/76beeb769e30adc912d648c014fd95bf748fef24/stew/result.nim#L238

like that, Result works as a transport to capture the current exception and pass it to a different stack frame (because it will rethrow the same exception), but I'd like the Exception type to be forwarded perfectly as well - think that's not common? think async/await where the Future does this (in fact, after a future has been completed, it is semantically the same thing as a Result.

Being able to reason about the deduced exceptions is pretty useful in generic code, as evidenced by nothrow(bool) support in C++ - it's very commonly used to differentiate code paths so that code that can be shown to be exception-free (and thus amenable to reasoning / optimization) can be more efficient and elegant thanks to stronger guarantees.

the callback problem happens when type erasure is involved, which is when the callback registration is dynamic - but there are plenty of cases where that's not the case.

arnetheduck commented 4 years ago

...though one has to wonder why no modern language tries to follow java's footsteps and actually put specific exceptions in signatures through raises - C++ removed them, rust and go didn't add them and neither did swift (except raises or not).. clearly, they're not very convenient all things considered ;)

Araq commented 4 years ago

There are seldom cases where it makes sense for a library to use exceptions instead of using errors or result/either. In my experience that's for libraries where consumers are not software engineers but domain experts like in ... This makes the error model part of the API (the raises: [MyNewException] is an alternative but in practice no one pushed it far enough to show it worked), this makes it easier to provide libraries to consume from other language, this avoids the mistake of Python of using exceptions for all control flow and only coding/testing for the happy path (i.e. all files are found, network connection is never lost, and there is always disk space).

That's a programming language design fashion, ymmv. In my opinion garbage collection and exception handling are what enabled Python to grow its impressive set of libraries in the first place. And are responsible for Python's success. And yes, also its dynamic typing helped as you can emulate in your custom class what is required by the function f which comes from a thirdparty dependency.

For most other cases (IO, streams, networking, serialization, ...), it makes more sense to use errors at the low-level and let/force consumer applications (not libraries) deal with the error.

That doesn't match my experience at all. Exceptions are useful when errors, including IO errors, are pervasive.

FedericoCeratto commented 4 years ago

the mistake of Python of using exceptions for all control flow and only coding/testing for the happy path (i.e. all files are found, network connection is never lost, and there is always disk space).

A lot of of mission critical software is written in Python and injecting faults during functional testing is common practice.

One of the main benefit of exception is constraining failure modes: turning both known and unexpected failures from a system failure (e.g. a process crashing out) into loss of functionality of a subsystem.

Araq commented 4 years ago

This RFC has been implemented, closing. For defect tracking or other new features / warnings /etc we can create new RFCs.