From c24c9966387a9ef982194d8f6f90bab168493212 Mon Sep 17 00:00:00 2001
From: Shaz Qadeer <shaz.qadeer@gmail.com>
Date: Sun, 24 Nov 2024 09:20:13 -0800
Subject: [PATCH] more comments

---
 Test/civl/large-samples/cache-coherence.bpl | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/Test/civl/large-samples/cache-coherence.bpl b/Test/civl/large-samples/cache-coherence.bpl
index 6d27fc094..0b1b208ff 100644
--- a/Test/civl/large-samples/cache-coherence.bpl
+++ b/Test/civl/large-samples/cache-coherence.bpl
@@ -1,6 +1,15 @@
 // RUN: %parallel-boogie -vcsSplitOnEveryAssert "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
+/*
+This example constructs a directory-based MESI cache coherence protocol.
+Many important details of a realistic protocol are modeled.
+- Individual steps taken by the cache and directory controllers are fine-grained.
+- Operations on the cache controller are non-blocking.
+- Multiple memory addresses may map to the same cache address.
+- A cache line may be evicted nondeterministically.
+*/
+
 type MemAddr;
 type CacheAddr;
 function Hash(MemAddr): CacheAddr;