When using a STL data structure allocated on the stack, we must make sure its
elements are allocated with the same allocator as the structure. For instance,
in a model-checking context, the stack is persistent (non-snapshotting), so any
stack-allocated std::vector should use the non-snapshotting allocator (i.e.,
MyAlloc).
At the same time, clarify CycleGraph and CycleNode classes by labelling them as
SNAPSHOTALLOC.
ASSERT(cv);
reads_from = act;
if (act != NULL && this->is_acquire()) {
ASSERT(cv);
reads_from = act;
if (act != NULL && this->is_acquire()) {
- std::vector<const ModelAction *> release_heads;
+ std::vector< const ModelAction *, MyAlloc<const ModelAction *> > release_heads;
model->get_release_seq_heads(this, &release_heads);
for (unsigned int i = 0; i < release_heads.size(); i++)
synchronize_with(release_heads[i]);
model->get_release_seq_heads(this, &release_heads);
for (unsigned int i = 0; i < release_heads.size(); i++)
synchronize_with(release_heads[i]);
#include <vector>
#include <inttypes.h>
#include <vector>
#include <inttypes.h>
class CycleNode;
class ModelAction;
class CycleNode;
class ModelAction;
void commitChanges();
void rollbackChanges();
void commitChanges();
void rollbackChanges();
private:
CycleNode * getNode(const ModelAction *);
private:
CycleNode * getNode(const ModelAction *);
private:
/** @brief The ModelAction that this node represents */
const ModelAction *action;
private:
/** @brief The ModelAction that this node represents */
const ModelAction *action;
* false otherwise
*/
bool ModelChecker::release_seq_head(const ModelAction *rf,
* false otherwise
*/
bool ModelChecker::release_seq_head(const ModelAction *rf,
- std::vector<const ModelAction *> *release_heads) const
+ std::vector< const ModelAction *, MyAlloc<const ModelAction *> > *release_heads) const
{
if (!rf) {
/* read from future: need to settle this later */
{
if (!rf) {
/* read from future: need to settle this later */
* @see ModelChecker::release_seq_head
*/
void ModelChecker::get_release_seq_heads(ModelAction *act,
* @see ModelChecker::release_seq_head
*/
void ModelChecker::get_release_seq_heads(ModelAction *act,
- std::vector<const ModelAction *> *release_heads)
+ std::vector< const ModelAction *, MyAlloc<const ModelAction *> > *release_heads)
{
const ModelAction *rf = act->get_reads_from();
bool complete;
{
const ModelAction *rf = act->get_reads_from();
bool complete;
while (it != list->end()) {
ModelAction *act = *it;
const ModelAction *rf = act->get_reads_from();
while (it != list->end()) {
ModelAction *act = *it;
const ModelAction *rf = act->get_reads_from();
- std::vector<const ModelAction *> release_heads;
+ std::vector< const ModelAction *, MyAlloc<const ModelAction *> > release_heads;
bool complete;
complete = release_seq_head(rf, &release_heads);
for (unsigned int i = 0; i < release_heads.size(); i++) {
bool complete;
complete = release_seq_head(rf, &release_heads);
for (unsigned int i = 0; i < release_heads.size(); i++) {
bool isfinalfeasible();
void check_promises(ClockVector *old_cv, ClockVector * merge_cv);
void get_release_seq_heads(ModelAction *act,
bool isfinalfeasible();
void check_promises(ClockVector *old_cv, ClockVector * merge_cv);
void get_release_seq_heads(ModelAction *act,
- std::vector<const ModelAction *> *release_heads);
+ std::vector< const ModelAction *, MyAlloc<const ModelAction *> > *release_heads);
void finish_execution();
bool isfeasibleprefix();
void set_assert() {asserted=true;}
void finish_execution();
bool isfeasibleprefix();
void set_assert() {asserted=true;}
bool r_modification_order(ModelAction *curr, const ModelAction *rf);
bool w_modification_order(ModelAction *curr);
bool release_seq_head(const ModelAction *rf,
bool r_modification_order(ModelAction *curr, const ModelAction *rf);
bool w_modification_order(ModelAction *curr);
bool release_seq_head(const ModelAction *rf,
- std::vector<const ModelAction *> *release_heads) const;
+ std::vector< const ModelAction *, MyAlloc<const ModelAction *> > *release_heads) const;
bool resolve_release_sequences(void *location);
ModelAction *diverge;
bool resolve_release_sequences(void *location);
ModelAction *diverge;