From a124fdeef4ab9a7bcadf8d601742619ec06db5e3 Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Fri, 6 Jul 2012 18:12:59 -0700 Subject: [PATCH] nodestack: add stub 'get_next_read_from()' function This is the start of providing functional model-checking reads-from relationships. It is a stub because it doesn't properly handle "backtracking" and replay for reads-from assignments. It will simply return the first element in may_read_from. --- nodestack.cc | 16 ++++++++++++++++ nodestack.h | 1 + 2 files changed, 17 insertions(+) diff --git a/nodestack.cc b/nodestack.cc index 10f7a72b..2416ed7c 100644 --- a/nodestack.cc +++ b/nodestack.cc @@ -130,6 +130,22 @@ void Node::add_read_from(const ModelAction *act) may_read_from.push_back(act); } +/** + * Gets the next 'may_read_from' action from this Node. Only valid for a node + * where this->action is a 'read'. + * @todo Perform reads_from backtracking/replay properly, so that this function + * may remove elements from may_read_from + * @return The first element in may_read_from + */ +const ModelAction * Node::get_next_read_from() { + const ModelAction *act; + ASSERT(!may_read_from.empty()); + act = may_read_from.front(); + /* TODO: perform reads_from replay properly */ + /* may_read_from.pop_front(); */ + return act; +} + void Node::explore(thread_id_t tid) { int i = id_to_int(tid); diff --git a/nodestack.h b/nodestack.h index c09b628b..11cbdfa8 100644 --- a/nodestack.h +++ b/nodestack.h @@ -44,6 +44,7 @@ public: Node * get_parent() const { return parent; } void add_read_from(const ModelAction *act); + const ModelAction * get_next_read_from(); void print(); void print_may_read_from(); -- 2.34.1