fix(modelchecker): make protopath cache safe for concurrent readers (#357)

ProtoPath.filesMap is a global cache populated lazily by every Processor
through GetProtoFieldByPath. The map was written without synchronization
(only the values are immutable; the map structure mutates on insert).
Today this is benign because all callers are sequential; once parallel
simulation workers exist, two concurrent first-touches of the same file
or path will trip Go's "concurrent map writes" runtime check.

Wrap reads in a fast RLock path and writes in a Lock path with a double-
check after acquiring the write lock (in case another goroutine populated
the entry while we were computing). The expensive GetFieldByPath/
convertToProto work runs outside the write lock so workers don't serialize
on it.

Adds a concurrent test that exercises 16 goroutines × 200 iterations to
make the locking contract explicit; it currently passes either way
because Go's runtime check is timing-sensitive and the rules_go race
build setup here did not appear to wire through, but the test will start
catching regressions once we wire race detection or extend the iteration
count.

Co-authored-by: jayaprabhakar <jayaprabhakar@gmail.com>
Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: 3 people

modelchecker/protopath.go

@@ -8,29 +8,50 @@ import (
 	"regexp"
 	"strconv"
 	"strings"
+	"sync"
 )
 
 var re = regexp.MustCompile(`Stmts\[\d+\]`)
 
 type ProtoPath struct {
-	// TODO(jayaprabhakar): A quick hack, fix this. It is safe because this field is immutable.
+	mu       sync.RWMutex
 	filesMap map[*ast.File]map[string]proto.Message
 }
+
 var protoPathInstance = &ProtoPath{filesMap: make(map[*ast.File]map[string]proto.Message)}
 
 func GetProtoFieldByPath(file *ast.File, location string) proto.Message {
-	if protoPathInstance.filesMap[file] == nil {
-		protoPathInstance.filesMap[file] = make(map[string]proto.Message)
-	} else if val, ok := protoPathInstance.filesMap[file][location]; ok {
-		return val
+	// Fast path: read-locked cache lookup. Parallel callers (e.g. parallel
+	// simulation workers) hit this most of the time once the cache is warm.
+	protoPathInstance.mu.RLock()
+	if inner, ok := protoPathInstance.filesMap[file]; ok {
+		if val, hit := inner[location]; hit {
+			protoPathInstance.mu.RUnlock()
+			return val
+		}
 	}
+	protoPathInstance.mu.RUnlock()
+
+	// Slow path: compute outside the lock (reflection on the read-only AST
+	// is safe without the lock), then insert under a write lock with a
+	// re-check in case a concurrent caller already populated the entry.
 	field := GetFieldByPath(file, location)
-	if field == nil {
-		protoPathInstance.filesMap[file][location] = nil
-		return nil
+	var protobuf proto.Message
+	if field != nil {
+		protobuf = convertToProto(field.Elem().Interface(), field.Type())
+	}
+
+	protoPathInstance.mu.Lock()
+	defer protoPathInstance.mu.Unlock()
+	inner, ok := protoPathInstance.filesMap[file]
+	if !ok {
+		inner = make(map[string]proto.Message)
+		protoPathInstance.filesMap[file] = inner
+	}
+	if existing, hit := inner[location]; hit {
+		return existing
 	}
-	protobuf := convertToProto(field.Elem().Interface(), field.Type())
-	protoPathInstance.filesMap[file][location] = protobuf
+	inner[location] = protobuf
 	return protobuf
 }
 

modelchecker/protopath_test.go

@@ -5,6 +5,7 @@ import (
 	"github.com/stretchr/testify/assert"
 	"github.com/stretchr/testify/require"
 	"google.golang.org/protobuf/encoding/protojson"
+	"sync"
 	"testing"
 )
 
@@ -77,6 +78,45 @@ func TestEndOfBlock(t *testing.T) {
 		EndOfBlock("Actions[0].Block.Stmts[0].AnyStmt.Block.Stmts[0].IfStmt.Branches[0].Block.Stmts[0]"))
 }
 
+// TestGetProtoFieldByPath_Concurrent exercises the cache under parallel reads
+// + writes. Run with `go test -race` to catch any locking regression. The
+// shared protoPathInstance cache is hit by every Processor; parallel
+// simulation workers must not race on it.
+func TestGetProtoFieldByPath_Concurrent(t *testing.T) {
+	file, err := readFileToAst()
+	require.Nil(t, err)
+
+	paths := []string{
+		"Actions[0]",
+		"Actions[0].Block",
+		"Actions[0].Block.Stmts[0]",
+		"Actions[0].Block.Stmts[0].AnyStmt",
+		"Actions[0].Block.Stmts[0].AnyStmt.Block",
+		"Actions[1]",
+		"Actions[1].Block",
+		"Actions[1].Block.Stmts[0]",
+		"Actions[1].Block.Stmts[0].AnyStmt",
+		"NonExistentPath[42]", // exercises the nil-result cache entry
+	}
+
+	const workers = 16
+	const iterations = 200
+
+	var wg sync.WaitGroup
+	wg.Add(workers)
+	for w := 0; w < workers; w++ {
+		go func() {
+			defer wg.Done()
+			for i := 0; i < iterations; i++ {
+				for _, p := range paths {
+					_ = GetProtoFieldByPath(file, p)
+				}
+			}
+		}()
+	}
+	wg.Wait()
+}
+
 func readFileToAst() (*ast.File, error) {
 	jsonFile := `
 {