Linked lists

[michaelmcinerney]

Test with seL4/seL4#1176

[Xaphiosis]

this proof looks like a struggle uphill both ways in the snow... any insight into why the rules are matching so badly? ccorres_symb_exec_l has 4 versions (2,3,and '), none of them help?

[michaelmcinerney]

I think this proof was copied from somewhere, and it had this rather unusual structure. Would it be better to try to rewrite this?

[Xaphiosis]

I'd say it's worth a try, but as it's copied, I'd say put it on your TODO list and like the FIXME move above do it in another PR.

[Xaphiosis]

I've reviewed the generic and AARCH64 files now (assuming the other arches are same and will have same commentary apply to them, except maybe ARM/ARM_HYP will be extra clunky).

This is really a tremendous amount of work, and the sea of red in IpcCancel_C was really nice to see. Compared to the amount of changes, I only have small nitpicks related to documentation, maintenance and some automation. Very nice work. I really hope it helps when it comes to merges into rt as well. Do you by any chance have a before/after of Refine and CRefine (on the same machine) for any arch so we can see how much performance improved?

[michaelmcinerney]

I've reviewed the generic and AARCH64 files now (assuming the other arches are same and will have same commentary apply to them, except maybe ARM/ARM_HYP will be extra clunky).

This is really a tremendous amount of work, and the sea of red in IpcCancel_C was really nice to see. Compared to the amount of changes, I only have small nitpicks related to documentation, maintenance and some automation. Very nice work. I really hope it helps when it comes to merges into rt as well. Do you by any chance have a before/after of Refine and CRefine (on the same machine) for any arch so we can see how much performance improved?

Thanks Raf. I haven't done a before/after, but we could still do that before this is merged. I have never run any benchmarks like Corey has before, but that might be fun to do.

I'm actually not expecting that much of a performance increase from this work. It seems like the corres proofs contain a lot of slow list reasoning (butlast and tl and so on always seem to be ugly). If people have ideas on how that can be improved then that would be great.

I think the main benefit of this work is a much nicer abstraction to work with, especially when it comes to something as difficult as a loop, like we have in tcbReleaseEnqueue. I think that if we did linked lists in this way for the endpoint queues, then we would see a massive increase in speed. All the infrastructure should already be there for that to happen, but it would still be a fairly hefty project to carry it out. Another benefit of doing the endpoint queues in this way would be that we could get rid of all the ctcb_queue_relation business, even deleting the TcbQueue file we have in CRefine.

[corlewis]

This is really a tremendous amount of work, and the sea of red in IpcCancel_C was really nice to see. Compared to the amount of changes, I only have small nitpicks related to documentation, maintenance and some automation. Very nice work. I really hope it helps when it comes to merges into rt as well. Do you by any chance have a before/after of Refine and CRefine (on the same machine) for any arch so we can see how much performance improved?

I'm actually not expecting that much of a performance increase from this work. It seems like the corres proofs contain a lot of slow list reasoning (butlast and tl and so on always seem to be ugly). If people have ideas on how that can be improved then that would be great.

Initial tests show a slight slowdown in Refine, like you've suggested. I'll report on CRefine tomorrow.

master:
  N = 10
  Average ARM Refine: (00:10:52 real, 01:06:14 cpu, 16.06GB)
  Standard Deviation: (00:00:19 real, 00:02:51 cpu, 2.42GB)
linked_list:
  N = 10
  Average ARM Refine: (00:12:19 real, 01:17:09 cpu, 15.42GB)
  Standard Deviation: (00:00:21 real, 00:03:09 cpu, 2.11GB)

[corlewis]

Initial tests show a slight slowdown in Refine, like you've suggested. I'll report on CRefine tomorrow.

CRefine was very inconsistent this time for some reason but it does look like its performance has improved.

master:
  N = 14
  Average ARM CRefine: (00:29:47 real, 03:29:03 cpu, 22.12GB)
  Standard Deviation: (00:02:16 real, 00:27:27 cpu, 0.30GB)
linked_list:
  N = 14
  Average ARM CRefine: (00:26:25 real, 03:13:37 cpu, 22.22GB)
  Standard Deviation: (00:01:46 real, 00:22:36 cpu, 0.21GB)

Overall, I think this will be a noticeable performance improvement, particularly as these sessions are built in parallel and so reducing the longer time of CRefine should be more of a benefit.

[Xaphiosis]

Overall, I think this will be a noticeable performance improvement, particularly as these sessions are built in parallel and so reducing the longer time of CRefine should be more of a benefit.

Thanks @corlewis ! The time saved in CRefine is nice indeed, even if overall it's only one wall-minute saved across both.

[lsf37]

Nice performance numbers! Pretty much as expected (slightly slower Refine, faster CRefine), but good to see that the CRefine speedup is a good bit more than the Refine slowdown. Quite happy with that!

[lsf37]

This is looking good for merge now from my side. We need to simultaneously merge the corresponding seL4 PR.