diff --git a/_CoqProject b/_CoqProject index dc9ec33770ae3d4d57e94526b20352919f5ddff6..5a389c306975fd587fbc98adc3c33bf94412bfbc 100644 --- a/_CoqProject +++ b/_CoqProject @@ -39,8 +39,8 @@ theories/logrel/session_typing_rules.v theories/logrel/napp.v theories/logrel/lib/mutex.v theories/logrel/lib/par_start.v -theories/logrel/examples/double.v theories/logrel/examples/pair.v +theories/logrel/examples/par_recv.v theories/logrel/examples/rec_subtyping.v theories/logrel/examples/choice_subtyping.v theories/logrel/examples/mapper.v diff --git a/papers/CPP21.md b/papers/CPP21.md index d763a0f64f0aa1c0a6811c1d9786047fe18b25cc..757dd284f4542667e85e90ccb28341c0e03fb246 100644 --- a/papers/CPP21.md +++ b/papers/CPP21.md @@ -15,7 +15,7 @@ ## Examples - The parallel receive example in Section 4 can be found in - [theories/logrel/examples/double.v](../theories/logrel/examples/double.v): + [theories/logrel/examples/par_recv.v](../theories/logrel/examples/par_recv.v): This program performs two ``racy'' parallel receives on the same channel from two different threads, using locks to allow the channel to be shared. - The parallel compute client example in Section 4 can be found in diff --git a/theories/logrel/examples/double.v b/theories/logrel/examples/par_recv.v similarity index 100% rename from theories/logrel/examples/double.v rename to theories/logrel/examples/par_recv.v