From 96cc6915859876bd9a5c1774a5195058c7c2442c Mon Sep 17 00:00:00 2001 From: Brian Demsky Date: Tue, 25 Sep 2012 10:12:38 -0700 Subject: [PATCH] add comments --- model.cc | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/model.cc b/model.cc index 03a0c68..8a80070 100644 --- a/model.cc +++ b/model.cc @@ -1097,8 +1097,15 @@ bool ModelChecker::release_seq_head(const ModelAction *rf, rel_heads_list_t *rel /** @todo Need to be smarter here... In the linux lock * example, this will run to the beginning of the program for * every acquire. */ + /** @todo The way to be smarter here is to keep going until 1 + * thread has a release preceded by an acquire and you've seen + * both. */ + if (rf->is_acquire() && rf->is_release()) return true; /* complete */ + + /** @todo Might it be better to make this into a loop... */ + return release_seq_head(rf->get_reads_from(), release_heads); } if (rf->is_release()) -- 2.34.1