Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

RFC: Global Conditions #2516

Merged
merged 9 commits into from
Jun 27, 2023
Merged

RFC: Global Conditions #2516

Changes from all commits
Commits
Show all changes
9 commits
Select commit Hold shift + click to select a range
48cc417
RFC: Global conditions
adpaco-aws Jun 12, 2023
8c2f50d
Address some comments
adpaco-aws Jun 14, 2023
368c329
Address Kareem's comments
adpaco-aws Jun 14, 2023
1ef6683
Remove comment about `kani-driver` code.
adpaco-aws Jun 14, 2023
e401bba
Update with link to proof of concept
adpaco-aws Jun 15, 2023
3935af4
Update with content on failed checks
adpaco-aws Jun 19, 2023
52d6e8d
Add clarification on enabling global conditions
adpaco-aws Jun 22, 2023
b8e61ee
Add separator
adpaco-aws Jun 23, 2023
1524e53
Edit status before merge
adpaco-aws Jun 27, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
111 changes: 111 additions & 0 deletions rfc/src/rfcs/0007-global-conditions.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,111 @@
- **Feature Name:** Global Conditions (`global-conditions`)
- **Feature Request Issue:** <https://github.com/model-checking/kani/issues/2525>
- **RFC PR:** <https://github.com/model-checking/kani/pull/2516>
- **Status:** *Unstable*
- **Version:** 0
- **Proof-of-concept:** <https://github.com/model-checking/kani/pull/2532>

-------------------

## Summary

A new section in Kani's output to summarize the status of properties that depend on other properties. We use the term *global conditions* to refer to such properties.
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

would "dependent conditions" be a better name than "global conditions" ?

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

So are global conditions solely defined as conjunctions of assert/cover statement or are there other ways of defining them ?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Not sure about the name.

Global conditions do not need to depend on assert/cover statements, and there should be other ways to define them. For example, one possibility we've discussed in the past is to have a memory-safety condition based on the result of all memory safety checks we currently produce.


## User Impact

The addition of new options that affect the overall verification result depending on certain property attributes demands some consideration.
In particular, the addition of a new option to fail verification if there are uncoverable (i.e., unsatisfiable or unreachable) `cover` properties (requested in [#2299](https://github.com/model-checking/kani/issues/2299)) is posing new challenges to our current architecture and UI.
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

What are the problems being addressed ?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm not sure if you're asking about the problems being addressed in Kani (to enable global conditions) or the problems being addressed with the feature requested in #2299 .

If it's the former, then the problem is that Kani isn't flexible enough. Until the #[kani::should_panic] attribute was introduced, there was only one way to get a successful verification: making all checks pass (i.e., getting a SUCCESS status in each of the individual checks/properties). But users may want to verify other things, or define additional conditions for verification like we're doing here.

If it's the latter, then the problem is vacuity. We check the status for cover properties, but their status doesn't impact verification in any way. Some users want to additionally ensure that the predicates in cover are always satisfied - the option requested in #2299 is for them.


This concept isn't made explicit in Kani, but exists in some ways.
For example, the `kani::should_panic` attribute is a global condition because it can be described in terms of other properties (checks).
The request in [#2299](https://github.com/model-checking/kani/issues/2299) is essentially another global conditions, and we may expect more to be requested in the future.

In this RFC, we propose a new section in Kani's output focused on reporting global conditions.
The goal is for users to receive useful information about hyperproperties without it becoming overwhelming.
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

is "hyperproperties" meant as in "a property that relates two or more executions of the same program?"

This will help users to understand better options that are enabled through global conditions and ease the addition of such options to Kani.

## User Experience

**The output will refer to properties that depend on other properties as "global conditions"**, which is a simpler term.
The options to enable different global conditions will depend on a case-by-case basis[^enable-options].

The main UI change in this proposal is a new `GLOBAL CONDITIONS` section that **won't be printed if no global conditions have been enabled**.
celinval marked this conversation as resolved.
Show resolved Hide resolved
This section will only appear in Kani's default output after the `RESULTS` section (used for individual checks) and have the format:

```
GLOBAL CONDITIONS:
- `<name>`: <status> (<reason>)
- `<name>`: <status> (<reason>)
[...]
```

where:
- `<name>` is the name given to the global condition.
- `<status>` is the status determined for the global condition.
- `<reason>` is an explanation that depends on the status of the global condition.

For example, let's assume we implement the option requested in [#2299](https://github.com/model-checking/kani/issues/2299).
A concrete example of this output would be:

```
GLOBAL CONDITIONS:
- `fail_uncoverable`: SUCCESS (all cover statements were satisfied as expected)
```

A `FAILED` status in any enabled global condition will cause verification to fail.
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Are global conditions only enabled using special flags or can the user also define his own groups of dependent conditions ?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Please note that those are two separate questions:

  1. Are global conditions only enabled using special flags?: No. Some may be enabled using special flags. Others may be enabled using attributes. Others may use a combination. We don't put constrains on this at the moment.
  2. Can the user also define his own groups of dependent conditions?: No, the RFC doesn't contemplate this option at the moment. That would require a language to define conditions.

In that case, the overall verification result will point out that one or more global conditions failed, as in:

```
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is it possible to list the basic conditions that failed to explain why a global condition failed ?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, it should be possible.

VERIFICATION:- FAILURE (one or more global conditions failed)
```

This last UI change will also be implemented for the terse output.
Finally, checks that cause an enabled global condition to fail will be reported using the same interface we use for failed checks[^failed-checks].

**Global conditions which aren't enabled won't appear in the `GLOBAL CONDITIONS` section**.
Their status will be computed regardless[^status-computation], and we may consider showing this status when the `--verbose` option is passed.

The documentation of global conditions will depend on how they're enabled, which depends on a case-by-case basis.
adpaco-aws marked this conversation as resolved.
Show resolved Hide resolved
However, we may consider adding a new subsection `Global conditions` to the `Reference` section that collects all of them so it's easier for users to consult all of them in one place.

## Detailed Design

The only component to be modified is `kani-driver` since that's where verification results are built and determined.
But we should consider moving this logic into another crate.

We don't need new dependencies.
The corner cases will depend on the specific global conditions to be implemented.

## Rationale and alternatives

As mentioned earlier, we're proposing this change to help users understand global conditions and how they're determined.
In many cases, global conditions empower users to write harnesses which weren't possible to write before.
As an example, the `#[kani::should_panic]` attribute allowed users to write harnesses expecting panic-related failures.
adpaco-aws marked this conversation as resolved.
Show resolved Hide resolved
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

the documentation of should_panic does not really give a precise meaning to the check, i.e. it does not say if at least one execution must trigger a panic or if all executions must trigger a panic. How can it be modelled in terms of dependent conditions and statuses ?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't think we do that for any of the checks we currently produce. Regardless, I think it's well defined in here, and if you think otherwise I'm happy to do any editions you consider appropriate.


Also, we don't really know if more global conditions will be requested in the future.
We may consider discarding this proposal and waiting for the next feature that can be implemented as a global condition to be requested.

### Alternative: Global conditions as regular checks

One option we've considered in the past is to enable global conditions as a regular checks.
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

What is a regular check ? kani::assert ? kani::cover ?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Check is the simpler term we use to refer to properties. Running Kani on any will output something like this:

RESULTS:
Check 1: example.assertion.1
         - Status: <status>
         - Description: <description>
         - Location: <location>
[...]

So this refers to those checks/properties.

While it's technically doable, it doesn't feel appropriate for global conditions to reported through regular checks since generally a higher degree of visibility may be appreciated.

## Open questions

No open questions.
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

is it possible to give a more explicit and rigorous definition of global conditions ?

e.g. "a global condition is specified by a set of assert or cover statements and an aggregation function that computes a status for the global conditions from the statuses of the basic conditions."

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Maybe? But it's definitely not that.

I'm actually thinking about growing the scope of global conditions to consider things other than other properties. For example, a timeout feature could be implemented a global condition. However, the current definition of global condition does not consider resources like memory or time, only verification properties.


## Future possibilities

A redesign of Kani's output is likely to change the style/architecture to report global conditions.

[^status-computation]: The results for global conditions would be computed during postprocessing based on the results of other checks.
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

so the status of a global condition could differ when the switch --fail-uncoverable is activated vs not activated ?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

No. The status computed for the condition itself won't differ. But activating the switch will simply cause the status of the global condition to affect the overall verification result.

Global conditions' checks aren't part of the SAT, therefore this computation won't impact verification time.

[^failed-checks]: We do not discuss the specific interface to report the failed checks because it needs improvements (for both global conditions and standard verification).
In particular, the description field is the only information printed for properties (such as `cover` statements) without trace locations.
There are additional improvements we should consider: printing the actual status (for global conditions, this won't always be `FAILED`), avoid the repetition of `Failed Checks: `, etc.
[This comment](https://github.com/model-checking/kani/pull/2516#issuecomment-1597524184) discusses problems with the current interface on some examples.

[^enable-options]: In other words, global conditions won't force a specific mechanism to be enabled.
For example, if the `#[kani::should_panic]` attribute is converted into a global condition, it will continue to be enabled through the attribute itself.
Other global conditions may be enabled through CLI flags only (e.g., `--fail-uncoverable`), or a combination of options in general.