diff --git a/_CoqProject b/_CoqProject index 348e6fa3e16916141565aa5591be6e21f4f4067a..dad39bbfe6414ba5812154a26864c4940de9c22b 100644 --- a/_CoqProject +++ b/_CoqProject @@ -20,7 +20,7 @@ theories/examples/basics.v theories/examples/sort.v theories/examples/sort_br_del.v theories/examples/sort_fg.v -theories/examples/map.v +theories/examples/par_map.v theories/examples/map_reduce.v theories/examples/swap_mapper.v theories/examples/subprotocols.v diff --git a/papers/POPL20.md b/papers/POPL20.md index 8a2b7224a161fd74995a9dcaa16ebcdfb3434d7b..258bc903b43775cdc364d40aff458981ecf2e09a 100644 --- a/papers/POPL20.md +++ b/papers/POPL20.md @@ -16,7 +16,7 @@ Tour of Actris - Dependent: [theories/examples/sort_fg.v](../theories/examples/sort_fg.v) Manifest sharing via locks - Sample program: [theories/examples/basics.v](../theories/examples/basics.v) - - Distributed mapper: [theories/examples/map.v](../theories/examples/map.v) + - Distributed mapper: [theories/examples/par_map.v](../theories/examples/par_map.v) Case study: map reduce: - Utilities for shuffling/grouping: [theories/utils/group.v](../theories/utils/group.v) - Implementation and verification: [theories/examples/map_reduce.v](../theories/examples/map_reduce.v) diff --git a/theories/examples/map_reduce.v b/theories/examples/map_reduce.v index 7e1ccfb7d51fef6fa65aebf7dd693c706b54b857..ce0b913eb6fbd22fab2d3bfaa9204be3be0072e0 100644 --- a/theories/examples/map_reduce.v +++ b/theories/examples/map_reduce.v @@ -2,7 +2,7 @@ specification thereof, and its proofs. *) From actris.channel Require Import proofmode. From actris.utils Require Import llist compare contribution group. -From actris.examples Require Import map sort_fg. +From actris.examples Require Import par_map sort_fg. From iris.algebra Require Import gmultiset. (** * Functional version of map reduce (aka the specification) *) diff --git a/theories/examples/map.v b/theories/examples/par_map.v similarity index 100% rename from theories/examples/map.v rename to theories/examples/par_map.v