On 11/20/20 5:21 PM, Klein, Gerwin (Data61, Kensington NSW) wrote:

Hi Iker,

I'm having certain issues with the PR where I propose another way to get the gic cpu id directly from hardware registers instead of guessing like before.

First of all: thanks for the PR! I assume you mean https://github.com/seL4/seL4/pull/283

First of all, inside CI/Links some errors appear about sel4 webpage links that I haven't touched, how can I solve this?

It’s Ok to ignore this one. Looking at the links that are failing, they have moved recently (yesterday), and we should update them in a separate PR.

At last, on the PR/Preprocess test failure appears but it's not clear what the problem is and after the compilation test is successful.

The preprocess test is indeed not yet well documented. Its purpose is to tell wether the proposed changes will change something in the verified configurations of seL4 and might therefore need proof updates.

I had planned to chain this test with a full proof run when it fails (the preprocess test just sees that something changed, but for many small changes the proof still works), but it turns out the github CI infrastructure is too weak to run the proofs (not enough memory on the test runners). We’re looking into using something else for that, maybe AWS, but I haven’t had time yet to actually do that (it’s non-trivial to set up, at least if you want to be able to prevent abuse, and AWS costs money of course).

So for now, the right course of action, which I’ll document next week, is to ask for help when the preprocess test fails, so that someone in the verification team can either review it or run the proofs to check if they still work.

If changes do break the proof, then we'd need to discuss how to verify them and who will do the work for it. Looking at your PR, I think they would be fine, but I’ll start a proof run and comment on the PR when it is done.

A couple of related questions: 1. Are formatting changes (whitespace, comments, etc) guaranteed to not break the proofs? 2. If a change does break the proofs, would you be willing to coach someone on fixing them?

Cheers, Gerwin

Sincerely, Demi

On 11/21/20 7:09 PM, Klein, Gerwin (Data61, Kensington NSW) wrote:

...

On 21 Nov 2020, at 11:36, Demi M. Obenour wrote:

Signed PGP part On 11/20/20 5:21 PM, Klein, Gerwin (Data61, Kensington NSW) wrote:

...

If changes do break the proof, then we'd need to discuss how to verify them and who will do the work for it. Looking at your PR, I think they would be fine, but I’ll start a proof run and comment on the PR when it is done.

A couple of related questions:

1. Are formatting changes (whitespace, comments, etc) guaranteed to not break the proofs?

Some comments are proof annotations. As long as those don’t change, other whitespace and comment change will not break the proofs.

...

2. If a change does break the proofs, would you be willing to coach someone on fixing them?

Yes, depending on the change. If it is a 10 person-year project less likely :-). If it is something small then usually yes.

Good to know. That makes me feel much better about my ability to contribute in the future, should my plans call for it.

Cheers, Gerwin