quick clean up pass on exercises/solutions

verus-lang · Nov 3, 2024 · f9a86d2 · f9a86d2
1 parent 7ac3e09
commit f9a86d2
Show file tree

Hide file tree

Showing 3 changed files with 8 additions and 7 deletions.
diff --git a/2024-sosp-tutorial/exercises/advanced-rust-topics/exercise_01_memoize.rs b/2024-sosp-tutorial/exercises/advanced-rust-topics/exercise_01_memoize.rs
@@ -109,7 +109,7 @@ fn todo<A>() -> A
 //
 // 1. Make `Memoizer` generic over Args, Output, and the computation.
 //
-// 2. The current locking scheme is very coarse-grained. Come up with (and implement) and more
-//    fine-grained scheme.
+// 2. The current locking scheme is very coarse-grained. Come up with (and implement) a more
+//    fine-grained locking scheme to reduce thread contention.
 
 }
diff --git a/2024-sosp-tutorial/exercises/advanced-rust-topics/solutions/solution_counting_to_2.rs b/2024-sosp-tutorial/exercises/advanced-rust-topics/solutions/solution_counting_to_2.rs
@@ -137,17 +137,17 @@ tokenized_state_machine!(
 
         #[inductive(tr_inc_a)]
         fn tr_inc_a_preserves_the_invariant(pre: Self, post: Self) {
-            /* proof here */
+            /* You can leave this empty */
         }
 
         #[inductive(tr_inc_b)]
         fn tr_inc_b_preserves_the_invariant(pre: Self, post: Self) {
-            /* proof here */
+            /* You can leave this empty */
         }
 
         #[inductive(initialize)]
         fn initial_state_satisfies_inv(post: Self) {
-            /* proof here */
+            /* You can leave this empty */
         }
     }
 );

diff --git a/2024-sosp-tutorial/exercises/advanced-rust-topics/solutions/solution_memoize.rs b/2024-sosp-tutorial/exercises/advanced-rust-topics/solutions/solution_memoize.rs
@@ -11,6 +11,7 @@ use vstd::rwlock::{RwLock, RwLockPredicate};
 use vstd::hash_map::HashMapWithView;
 use std::sync::Arc;
 
+#[path = "../memoization_exercise_internals.rs"]
 mod memoization_exercise_internals;
 
 verus!{
@@ -123,7 +124,7 @@ fn todo<A>() -> A
 //
 // 1. Make `Memoizer` generic over Args, Output, and the computation.
 //
-// 2. The current locking scheme is very coarse-grained. Come up with (and implement) and more
-//    fine-grained scheme.
+// 2. The current locking scheme is very coarse-grained. Come up with (and implement) a more
+//    fine-grained locking scheme to reduce thread contention.
 
 }