diff --git a/src/Makefile.am b/src/Makefile.am index 908212ba..89d0cd15 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -70,6 +70,7 @@ slim_SOURCES = \ ext/init_exts.cpp \ ext/integer.cpp \ ext/float.cpp \ + ext/atomic.cpp \ ext/nlmem.cpp \ ext/array.cpp ext/array.h \ ext/atom.cpp \ diff --git a/src/ext/atomic.cpp b/src/ext/atomic.cpp new file mode 100644 index 00000000..e3b4204c --- /dev/null +++ b/src/ext/atomic.cpp @@ -0,0 +1,384 @@ +/* + * atomic.cpp + * + * Copyright (c) 2008, Ueda Laboratory LMNtal Group + * + * All rights reserved. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are + * met: + * + * 1. Redistributions of source code must retain the above copyright + * notice, this list of conditions and the following disclaimer. + * + * 2. Redistributions in binary form must reproduce the above copyright + * notice, this list of conditions and the following disclaimer in + * the documentation and/or other materials provided with the + * distribution. + * + * 3. Neither the name of the Ueda Laboratory LMNtal Group nor the + * names of its contributors may be used to endorse or promote + * products derived from this software without specific prior + * written permission. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS + * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT + * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR + * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT + * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, + * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT + * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, + * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY + * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT + * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE + * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + * + * $Id$ + */ + +#include "../lmntal.h" +#include "verifier/verifier.h" +#include "vm/vm.h" +#ifdef PROFILE +#include "verifier/runtime_status.h" +#endif +#include "vm/react_context.hpp" + +namespace c14 = slim::element; + +void atomic_ruleset(LmnReactCxtRef rc, LmnMembraneRef mem, LmnAtomRef a0, + LmnLinkAttr t0) { + + if (LMN_INT_ATTR == t0) { + int i, n = mem->ruleset_num(); + AtomicType atomic_type; + + switch ((LmnWord)a0) { + case 1: + atomic_type = ATOMIC_ALL_EXHAUSTIVE; + break; + case 2: + atomic_type = ATOMIC_SIMULATION; + break; + case 3: + atomic_type = ATOMIC_SYNC_STEP; + break; + default: + atomic_type = ATOMIC_NONE; + break; + } + + for (i = 0; i < n; i++) { + lmn_mem_get_ruleset(mem, i)->atomic = atomic_type; + lmn_mem_add_ruleset(mem->mem_parent(), + new LmnRuleSet(*lmn_mem_get_ruleset(mem, i))); + } + lmn_mem_delete_atom(mem, a0, t0); + } + + if (rc->has_mode(REACT_MEM_ORIENTED)) { + ((MemReactContext*)rc)->memstack_remove(mem); + } + mem->mem_parent()->remove_mem(mem); +} + +void init_atomic(void) { + CCallback::lmn_register_c_fun("atomic_ruleset", (void *)atomic_ruleset, 1); +} + +/* this function applies rules in $rs to $mem as much as possible */ +static inline BOOL react_ruleset_AMAP(LmnReactCxtRef rc, LmnMembraneRef mem, + LmnRuleSetRef rs) { + BOOL ret = FALSE; + for (int i = 0; i < rs->size(); i++) { + LmnRuleRef r = rs->get_rule(i); +#ifdef PROFILE + if (!lmn_env.nd && lmn_env.profile_level >= 2) { + profile_rule_obj_set(rs, r); + } +#endif + if (Task::react_rule(rc, mem, r)) { + i = 0; + ret = TRUE; + } + } + return ret; +} + +static inline LmnWorker *build_atomic_worker() { + LmnWorker *w; + StateSpaceRef sub_states; + BYTE sub_flags = 0x00U; + + mc_set_compress(sub_flags); + sub_states = new StateSpace(NULL, NULL); + w = lmn_worker_make(sub_states, env_my_thread_id(), sub_flags); + dfs_env_set(w); + worker_init(w); + worker_rc(w) = c14::make_unique(nullptr); + + + /* TODO: ここで作ったLmnWorkerは所属groupがNULLのため, + * atomic stepで更なる並列実行はできない */ + + return w; +} + +static inline void abort_atomic_worker(LmnWorker *w) { + // delete (worker_states(w)); + // delete (worker_rc(w)); + lmn_worker_free(w); +} + +/* ルールセットat_setの各ルールを可能な限り適用する. + * 非決定実行時には状態遷移のサブグラフを構築し, + * 停止状態をmemの遷移先として生成し, rcに登録する. */ +static BOOL react_ruleset_atomic_all(MCReactContext* rc, LmnMembraneRef mem, + LmnRuleSetRef at_set) { + unsigned int i, n, succ_i_from; + at_set->validate_atomic(); + + succ_i_from = mc_react_cxt_expanded_num(rc); + for (auto r : *at_set) + Task::react_rule(rc, mem, r); + + n = mc_react_cxt_expanded_num(rc) - succ_i_from; + if (n > 0) { + LmnWorker *w = build_atomic_worker(); + worker_rc(w)->start_atomic_step(at_set->id); + for (i = 0; i < n; i++) { + State *sub_s = + new State((LmnMembraneRef)rc->expanded_pop(), + DEFAULT_STATE_ID, (worker_states(w))->use_memenc()); + if (sub_s != (worker_states(w))->insert(sub_s)) { + delete (sub_s); + } else { + worker_states(w)->set_init_state(sub_s); + dfs_start(w); + } + } + + /* サブルーチン側であるatomic workerの並列実行は想定していないので, + * 以下の記述でもok */ + auto ends = (worker_states(w))->end_states; + for (i = 0; i < ends.size(); i++) { + for (int j = 0; j < ends[i].size(); j++) { + LmnMembraneRef end_m = + lmn_binstr_decode(((State *)ends[i][j])->state_binstr()); + mc_react_cxt_add_expanded((MCReactContext*)rc, end_m, new LmnRule()); + } + } + // RC_FINISH_ATOMIC_STEP(&WORKER_RC(w)); /* + // どうせ破棄しちゃうから要らない */ + abort_atomic_worker(w); + } + + at_set->invalidate_atomic(); + return succ_i_from != mc_react_cxt_expanded_num((MCReactContext*)rc); +} + +/* ルールセットat_setの各ルールを昇順にちょうど1stepずつ展開する. + * 適用のなかったルールはskip. + * ex) + * --------- + * a(0). + * { '$callback'(atomic_ruleset, 3). + * ruleA @@ a(X) :- X>0, Y=X+1 | a(Y). + * ruleB @@ a(X) :- a(X), b. + * ruleC @@ a(5) :- ok. + * } + * --------- + * result: ok, b, b, b, b, b. + */ +static BOOL react_ruleset_atomic_sync(LmnReactCxtRef rc, LmnMembraneRef mem, + LmnRuleSetRef at_set) { + BOOL ret; + + if (!rc->has_mode(REACT_ND)) { + for (auto r : *at_set) { + if (Task::react_rule(rc, mem, r)) { + return true; + } + } + return false; + } + + unsigned int r_i, succ_i_from; + BYTE mode_org; + LmnMembraneRef groot_m; + MCReactContext* mcrc = ((MCReactContext*)rc); + + succ_i_from = mc_react_cxt_expanded_num(mcrc); + + /* 1step目: generate successor membrane */ + for (r_i = 0; r_i < at_set->size(); r_i++) { + Task::react_rule(rc, mem, at_set->get_rule(r_i)); + if (mc_react_cxt_expanded_num(mcrc) > succ_i_from) { + r_i++; + break; + } + } + + /* ND モードでの Process ID のリセットをオーバーライド */ + env_set_next_id(rc->get_proc_next_id()); + + if (r_i < at_set->size()) { + at_set->validate_atomic(); + mode_org = rc->mode; + groot_m = rc->get_global_root(); + rc->set_mode(REACT_STAND_ALONE); + + /* ignore all but the last reaction */ + LmnMembraneRef succ_m; + + LmnRuleRef succ_r = (LmnRuleRef) mcrc->pop_expanded_rule(); + if (mcrc->has_optmode(DeltaMembrane)) { + succ_m = (LmnMembraneRef) mcrc->pop_mem_delta_root(); + } else { + succ_m = (LmnMembraneRef) mcrc->pop_expanded_state(); + } + while (succ_i_from < mc_react_cxt_expanded_num(mcrc)) { + mcrc->expanded_pop(); + } + mc_react_cxt_add_expanded(mcrc, succ_m, succ_r); + + /* 2〜r_n step目 */ + // for (i = succ_i_from; i < mc_react_cxt_expanded_num(rc); i++) { + + // restore the current membrane of the last reaction + LmnMembraneRef cur_mem = rc->get_cur_mem(); + + mcrc->set_global_root(succ_m); + react_ruleset_AMAP(rc, cur_mem, system_ruleset); + for (int j = r_i; j < at_set->size(); j++) { + if (Task::react_rule(rc, cur_mem, at_set->get_rule(j))) { + react_ruleset_AMAP(rc, cur_mem, system_ruleset); + } + } + // } + + mcrc->set_global_root(groot_m); + rc->set_mode(mode_org); + at_set->invalidate_atomic(); + } + + env_set_next_id(rc->get_proc_org_id()); + ret = FALSE; + + return ret; +} + +/* ルールセットat_setのルールを書換えが停止するまで繰返し適用する． + * ルールセットの停止性と合流性を仮定している．非決定モードでも + * 複数の書換え経路の探索は行わない． + */ +static inline BOOL react_ruleset_atomic_simulation(LmnReactCxtRef rc, + LmnMembraneRef mem, + LmnRuleSetRef at_set) { + BOOL ret; + + if (!rc->has_mode(REACT_ND)) { + ret = FALSE; + while (react_ruleset_AMAP(rc, mem, at_set) || + react_ruleset_AMAP(rc, mem, system_ruleset)) { + ret = TRUE; + } + } else { + unsigned int i, j, succ_i_from; + BYTE mode_org; + LmnMembraneRef groot_m; + MCReactContext* mcrc = (MCReactContext*) rc; + + succ_i_from = mc_react_cxt_expanded_num(mcrc); + /* 1step目: generate successor membrane */ + for (auto r : *at_set) { + Task::react_rule(rc, mem, r); + if (mc_react_cxt_expanded_num(mcrc) > succ_i_from) { + break; + } + } + + /* ND モードでの Process ID のリセットをオーバーライド */ + env_set_next_id(rc->get_proc_next_id()); + + if (i < at_set->size()) { + at_set->validate_atomic(); + mode_org = rc->mode; + groot_m = rc->get_global_root(); + rc->set_mode(REACT_STAND_ALONE); + + /* ignore all but the last reaction */ + LmnMembraneRef succ_m; + + LmnRuleRef succ_r = (LmnRuleRef) mcrc->pop_expanded_rule(); + if (mcrc->has_optmode(DeltaMembrane)) { + succ_m = (LmnMembraneRef) mcrc->pop_mem_delta_root(); + } else { + succ_m = (LmnMembraneRef) mcrc->pop_expanded_state(); + } + while (succ_i_from < mc_react_cxt_expanded_num(mcrc)) { + mcrc->expanded_pop(); + } + mc_react_cxt_add_expanded(mcrc, succ_m, succ_r); + + /* 2〜r_n step目 */ + // for (i = succ_i_from; i < mc_react_cxt_expanded_num(rc); i++) { + + // restore the current membrane of the last reaction + LmnMembraneRef cur_mem = rc->get_cur_mem(); + BOOL reacted; + + mcrc->set_global_root(succ_m); + react_ruleset_AMAP(rc, cur_mem, system_ruleset); + reacted = TRUE; + while (reacted) { + reacted = FALSE; + for (j = 0; j < at_set->size(); j++) { + reacted = reacted || Task::react_rule(rc, cur_mem, at_set->get_rule(j)); + } + if (reacted) { + react_ruleset_AMAP(rc, cur_mem, system_ruleset); + } + } + // } + mcrc->set_global_root(groot_m); + rc->set_mode(mode_org); + at_set->invalidate_atomic(); + } + + env_set_next_id(rc->get_proc_org_id()); + ret = FALSE; + } + + return ret; +} + +BOOL react_ruleset_atomic(LmnReactCxtRef rc, LmnMembraneRef mem, + LmnRuleSetRef rs) { + BOOL result = FALSE; + + if (rc->has_mode(REACT_ND) && ((MCReactContext*)rc)->has_optmode(DeltaMembrane)) { + lmn_fatal("unsupported delta-membrane, atomic step"); + } + + rc->start_atomic_step(rs->id); + switch (rs->atomic) { + case ATOMIC_SYNC_STEP: + result = react_ruleset_atomic_sync(rc, mem, rs); + break; + case ATOMIC_ALL_EXHAUSTIVE: + if (rc->has_mode(REACT_ND)) { + result = react_ruleset_atomic_all((MCReactContext*)rc, mem, rs); + } /* + else FALLTHROUTH */ + case ATOMIC_SIMULATION: + result = react_ruleset_atomic_simulation(rc, mem, rs); + break; + default: + lmn_fatal("unexpected react testing"); + break; + } + rc->finish_atomic_step(); + return result; +} diff --git a/src/ext/init_exts.cpp b/src/ext/init_exts.cpp index bf46ddd4..e99daf25 100644 --- a/src/ext/init_exts.cpp +++ b/src/ext/init_exts.cpp @@ -45,6 +45,7 @@ void init_integer(void); void init_float(void); void init_nlmem(void); +void init_atomic(void); void init_initial_ruleset(void); void init_nd_conf(void); void init_time(void); @@ -58,6 +59,7 @@ void init_builtin_extensions(void) init_integer(); init_float(); init_nlmem(); + init_atomic(); init_initial_ruleset(); init_nd_conf(); init_time(); diff --git a/src/loader/so.h b/src/loader/so.h index 0392797c..0390d3ac 100644 --- a/src/loader/so.h +++ b/src/loader/so.h @@ -175,6 +175,9 @@ for (i = 0; i < v.size(); i++) { \ LmnRuleSetRef cp = new LmnRuleSet(*(v[i])); \ lmn_mem_add_ruleset((LmnMembraneRef)rc->wt(destmemi), cp); \ + if (rc->has_mode(REACT_ATOMIC)) { \ + cp->invalidate_atomic(); \ + } \ } \ } while (0) diff --git a/src/verifier/statespace.h b/src/verifier/statespace.h index 875fd807..0af32cef 100644 --- a/src/verifier/statespace.h +++ b/src/verifier/statespace.h @@ -114,6 +114,7 @@ struct StateSpace : public std::conditional> end_states; /* 最終状態の集合 */ private: bool using_memenc; @@ -141,8 +142,6 @@ struct StateSpace : public std::conditional> end_states; /* 最終状態の集合 */ - std::unique_ptr &insert_destination(State *s, unsigned long hashv); std::unique_ptr &resize_destination(std::unique_ptr &def, State *ret, State *s); }; diff --git a/src/vm/react_context.hpp b/src/vm/react_context.hpp index 8f3728aa..144f9506 100644 --- a/src/vm/react_context.hpp +++ b/src/vm/react_context.hpp @@ -149,12 +149,21 @@ struct RuleContext { #define REACT_STAND_ALONE (0x01U << 2) /* 非決定実行: 状態は展開しない */ #define REACT_PROPERTY \ (0x01U << 3) /* LTLモデル検査: 性質ルールのマッチングのみ */ +#define REACT_ATOMIC (0x01U << 4) /* Atomic Step中: インタリーブの抑制 */ struct LmnReactCxt : slim::vm::RuleContext { LmnMembrane *global_root; /* ルール適用対象となるグローバルルート膜. != wt[0] */ private: unsigned int trace_num; /* ルール適用回数 (通常実行用トレース実行で使用) */ + + // 以下、atomic_ruleset周り + LmnRulesetId atomic_id; /* atomic step中: atomic set id(signed int), default:-1 */ + ProcessID proc_org_id; /* atomic step終了時に Process ID をこの値に復帰 */ + ProcessID proc_next_id; /* atomic step継続時に Process ID をこの値に設定 */ + LmnMembraneRef cur_mem; /* atomic step継続時に現在膜をこの値に設定 */ + BYTE flag; /* mode以外に指定するフラグ */ + public: BYTE mode; bool is_zerostep; @@ -167,23 +176,38 @@ struct LmnReactCxt : slim::vm::RuleContext { LmnReactCxt() : is_zerostep(false), keep_process_id_in_nd_mode(false), trace_num(0) {} LmnReactCxt(LmnMembrane *groot, BYTE mode) : is_zerostep(false), keep_process_id_in_nd_mode(false), trace_num(0), - mode(mode), global_root(groot) { + mode(mode), global_root(groot), flag(0x00U), atomic_id(-1) { } LmnReactCxt &operator=(const LmnReactCxt &from) { this->RuleContext::operator=(from); this->mode = from.mode; this->global_root = from.global_root; + this->flag = from.flag; + this->atomic_id = from.atomic_id; return *this; } unsigned int get_reaction_count() const { return trace_num; } void increment_reaction_count() { trace_num++; } + // 以下、atomic_ruleset周り + void start_atomic_step(LmnRulesetId id) { atomic_id = id; } + bool is_atomic_step() { return atomic_id >= 0; } + void finish_atomic_step() { atomic_id = -1; } + ProcessID get_proc_org_id() { return proc_org_id; } + void set_proc_org_id(ProcessID id) { proc_org_id = id; } + ProcessID get_proc_next_id() { return proc_next_id; } + void set_proc_next_id(ProcessID id) { proc_next_id = id; } + LmnMembraneRef get_cur_mem() { return cur_mem; } + void set_cur_mem(LmnMembraneRef mem) { cur_mem = mem; } + bool has_mode(BYTE mode) const { return (this->mode & mode) != 0; } + void set_mode(BYTE mode) { this->mode = mode; } + LmnMembrane *get_global_root() { return global_root; } SimpleHashtbl *get_hl_sameproccxt() { return hl_sameproccxt; } }; @@ -361,7 +385,12 @@ struct MCReactContext : LmnReactCxt { void push_expanded_state(void *s) { roots.push_back(s); } - + LmnWord pop_expanded_state() { + auto s = roots.back(); + roots.pop_back(); + return (LmnWord)s; + } + LmnRule *get_expanded_rule(int i) { return rules.at(i); } @@ -371,6 +400,11 @@ struct MCReactContext : LmnReactCxt { void push_expanded_rule(LmnRule *rule) { rules.push_back(rule); } + LmnWord pop_expanded_rule() { + auto ret = rules.back(); + rules.pop_back(); + return (LmnWord)ret; + } void clear_expanded_rules() { rules.clear(); } @@ -401,6 +435,21 @@ struct MCReactContext : LmnReactCxt { mem_deltas.push_back(root); } + LmnWord pop_mem_delta_root() { + auto d = mem_deltas.back(); + mem_deltas.pop_back(); + return (LmnWord)d; + } + + LmnWord expanded_pop(){ + pop_expanded_rule(); + if (this->has_optmode(DeltaMembrane)){ + return pop_mem_delta_root(); + } else { + return pop_expanded_state(); + } + } + private: /* 1. 遷移先計算中 * 通常: struct LmnMembrane diff --git a/src/vm/rule.hpp b/src/vm/rule.hpp index c5c53ca0..b2eb2a8c 100644 --- a/src/vm/rule.hpp +++ b/src/vm/rule.hpp @@ -166,6 +166,13 @@ class LmnRule { } }; +enum AtomicType { + ATOMIC_NONE = 0, + ATOMIC_ALL_EXHAUSTIVE, + ATOMIC_SIMULATION, + ATOMIC_SYNC_STEP, +}; + /* structure of RuleSet */ class LmnRuleSet { bool is_copied; @@ -175,18 +182,23 @@ class LmnRuleSet { std::vector subrules; bool ruleset_cp_is_need_object() const { - return has_unique(); + return has_unique() || (atomic != ATOMIC_NONE); } public: LmnRulesetId id; + AtomicType atomic; /* 本ルールセットの適用をatomicに実行するか否かを示すフラグ */ + bool is_atomic_valid; /* atomic step中であることを主張するフラグ */ LmnRuleSet(LmnRulesetId id, int init_size) : id(id), is_copied(false), - has_uniqrule(false), is_0step(false) {} + has_uniqrule(false), is_0step(false), + atomic(ATOMIC_NONE),is_atomic_valid(false) {} LmnRuleSet(const LmnRuleSet &rs) : LmnRuleSet(rs.id, rs.rules.capacity()) { is_copied = true; + atomic = rs.atomic; + is_atomic_valid = rs.is_atomic_valid; is_0step = rs.is_0step; /* ルール単位のオブジェクト複製 */ @@ -266,9 +278,12 @@ class LmnRuleSet { return ret; } + void validate_atomic() { is_atomic_valid = true; } + void invalidate_atomic() { is_atomic_valid = false; } void validate_zerostep() { is_0step = true; } bool is_zerostep() const { return is_0step; } + bool is_atomic() const { return is_atomic_valid; } bool is_copy() const { return is_copied; } bool has_unique() const { return has_uniqrule; } diff --git a/src/vm/task.cpp b/src/vm/task.cpp index 64090a98..38f20f51 100644 --- a/src/vm/task.cpp +++ b/src/vm/task.cpp @@ -125,6 +125,8 @@ struct Vector user_system_rulesets; /* system ruleset defined by user */ static inline BOOL react_ruleset(LmnReactCxtRef rc, LmnMembraneRef mem, LmnRuleSetRef ruleset); +static inline BOOL react_ruleset_inner(LmnReactCxtRef rc, LmnMembraneRef mem, + LmnRuleSetRef rs); static inline void react_initial_rulesets(LmnReactCxtRef rc, LmnMembraneRef mem); static inline BOOL react_ruleset_in_all_mem(LmnReactCxtRef rc, LmnRuleSetRef rs, @@ -344,7 +346,7 @@ BOOL Task::react_all_rulesets(LmnReactCxtRef rc, LmnMembraneRef cur_mem) { /* 通常実行では, 適用が発生しなかった場合にシステムルールの適用を行う * ndではokはFALSEなので, system_rulesetが適用される. */ - ok = ok || react_ruleset(rc, cur_mem, system_ruleset); + ok = ok || react_ruleset_inner(rc, cur_mem, system_ruleset); #ifdef USE_FIRSTCLASS_RULE lmn_rc_execute_insertion_events(rc); @@ -353,6 +355,10 @@ BOOL Task::react_all_rulesets(LmnReactCxtRef rc, LmnMembraneRef cur_mem) { return ok; } +/* an extenstion rule applier, @see ext/atomic.c */ +BOOL react_ruleset_atomic(LmnReactCxtRef rc, LmnMembraneRef mem, + LmnRuleSetRef rs); + /** 膜memに対してルールセットrsの各ルールの適用を試みる. * 戻り値: * 通常実行では, 書換えに成功した場合にTRUE, @@ -361,7 +367,29 @@ BOOL Task::react_all_rulesets(LmnReactCxtRef rc, LmnMembraneRef cur_mem) { */ static inline BOOL react_ruleset(LmnReactCxtRef rc, LmnMembraneRef mem, LmnRuleSetRef rs) { - + BOOL result; + + if (rc->is_atomic_step()) { + /* atomic_step時: atomic stepが複数ある場合, + * atomic適用中のrulesetとそうでないものを区別する必要がある + */ + if (rs->is_atomic()) { + result = react_ruleset_inner(rc, mem, rs); + } else { + result = FALSE; + } + } else if (rs->atomic == ATOMIC_NONE) { + result = react_ruleset_inner(rc, mem, rs); + } else { + result = react_ruleset_atomic(rc, mem, rs); + } + + return result; +} + +/** @see react_ruleset (task.c) */ +static inline BOOL react_ruleset_inner(LmnReactCxtRef rc, LmnMembraneRef mem, + LmnRuleSetRef rs) { //shuffle_ruleオプションが付いている場合はruleをシャッフル if(lmn_env.shuffle_rule) rs->shuffle(); @@ -1106,6 +1134,8 @@ bool slim::vm::interpreter::exec_command(LmnReactCxt *rc, LmnRuleRef rule, if (lmn_env.find_atom_parallel) return FALSE; + + // std::cout << instr_spec.at((LmnInstruction)op).op_str << std::endl; switch (op) { case INSTR_SPEC: { @@ -1410,8 +1440,16 @@ bool slim::vm::interpreter::exec_command(LmnReactCxt *rc, LmnRuleRef rule, rule->undo_history(); rc->warray_set(std::move(*tmp)); + // アトミック実行の際にProcess Idのリセットを一旦撤回するために + // 現在の Process ID と戻すべき Process ID を記録しておく + rc->set_proc_next_id(env_next_id()); + rc->set_proc_org_id(org_next_id); if (!rc->keep_process_id_in_nd_mode) env_set_next_id(org_next_id); + + /* 反応中の膜も記録しておく */ + rc->set_cur_mem((LmnMembraneRef) rc->wt(0)); + delete tmp; return command_result::Failure; }); @@ -4003,6 +4041,10 @@ bool slim::vm::interpreter::exec_command(LmnReactCxt *rc, LmnRuleRef rule, for (auto &rs : v) { auto cp = new LmnRuleSet(*rs); lmn_mem_add_ruleset((LmnMembraneRef)rc->wt(destmemi), cp); + if (rc->has_mode(REACT_ATOMIC)) { + /* atomic step中にatomic setをコピーした場合のため */ + cp->invalidate_atomic(); + } } break; }