From 9b894e117ad1090ad6f54753cde7fd9b6ea60ab7 Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Sun, 7 Oct 2012 23:24:21 -0700 Subject: [PATCH] model: add todo synchronization comment --- model.cc | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/model.cc b/model.cc index e23e9ec0..8267377f 100644 --- a/model.cc +++ b/model.cc @@ -576,6 +576,16 @@ void ModelChecker::process_relseq_fixup(ModelAction *curr, work_queue_t *work_qu ASSERT(release->same_thread(rf)); if (write == NULL) { + /** + * @todo Forcing a synchronization requires that we set + * modification order constraints. For instance, we can't allow + * a fixup sequence in which two separate read-acquire + * operations read from the same sequence, where the first one + * synchronizes and the other doesn't. Essentially, we can't + * allow any writes to insert themselves between 'release' and + * 'rf' + */ + /* Must synchronize */ if (!acquire->synchronize_with(release)) { set_bad_synchronization(); -- 2.34.1