[Civl] Cleaned up the ticket sample #818
Conversation
added layers for local tid introduced auxiliary globals at layer 1
There was a problem hiding this comment.
So one change here is the removal of the top level main procedure that calls Customer in a loop, and the necessary linear allocation code. Wondering why that isn't something useful to illustrate?
It seems there are other orthogonal improvements, like introducing the tid parameters, but I don't get the high-level picture. What is it?
| @@ -10,8 +10,8 @@ type {:linear "tid"} X; | |||
| const nil: X; | |||
There was a problem hiding this comment.
I think it would be nice to replace this with Option<_> from the library. (And rename X to Tid.)
There was a problem hiding this comment.
Good idea. Will do.
|
@menesro suggested using the ticket example to be the primary illustrator of all Civl machinery except permissions in the upcoming POPL 2024 tutorial. He made slides explaining the example. I was trying to change the code to become closer to the exposition. In particular, I dropped all the allocation of thread identifiers from the sample because permissions (specifically redistribution) will be explained in a more comprehensive using other examples (to be determined) and there is plenty going on in this example already. Adding main back might still be useful. Suggestions about the tutorial section on permissions are welcome. |
|
@bkragl : BTW, I stopped writing PR summaries since I didn't think anybody was paying attention :-). But every once in a while you pop in with some insightful question or comment. Do you actually look at the Civl PRs regularly? |
|
I do go over my github notifications, but often this happens in bursts. I try and see if I have the necessary context to contribute something, which unfortunately does not seem that often these days. I guess it's more likely for examples than it is for changes in the code. I understand that this is not a big motivation to write elaborate PR descriptions. |
|
Here is a PR: #828 |
No description provided.