From 1ae7b0ae07ee260bed68e10686a6e8223a550137 Mon Sep 17 00:00:00 2001 From: jayaprabhakar Date: Tue, 19 May 2026 12:34:12 -0700 Subject: [PATCH] fix(modelchecker): make protopath cache safe for concurrent readers MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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: Claude Opus 4.7 (1M context) --- modelchecker/protopath.go | 41 +++++++++++++++++++++++++--------- modelchecker/protopath_test.go | 40 +++++++++++++++++++++++++++++++++ 2 files changed, 71 insertions(+), 10 deletions(-) diff --git a/modelchecker/protopath.go b/modelchecker/protopath.go index 0242458..a282779 100644 --- a/modelchecker/protopath.go +++ b/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 } diff --git a/modelchecker/protopath_test.go b/modelchecker/protopath_test.go index 1640a23..45832af 100644 --- a/modelchecker/protopath_test.go +++ b/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 := ` {