Mercurial > hg > Papers > 2021 > kono-sigos
view src/PhilsImpl2.cbc @ 0:67e6ca3c7e6c
model checking
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Tue, 27 Apr 2021 14:25:56 +0900 |
parents | |
children |
line wrap: on
line source
Phils* createPhilsImpl(struct Context* context, int id, AtomicT_int* right, AtomicT_int* left) { struct Phils* phils = new Phils(); struct PhilsImpl* phils_impl = new PhilsImpl(); phils->phils = (union Data*)phils_impl; phils_impl->Leftfork = left; phils_impl->Rightfork = right; phils_impl->self = id; phils->putdown_lfork = C_putdown_lforkPhilsImpl; phils->putdown_rfork = C_putdown_rforkPhilsImpl; phils->eating = C_eatingPhilsImpl; phils->pickup_rfork = C_pickup_rforkPhilsImpl; phils->pickup_lfork = C_pickup_lforkPhilsImpl; phils->thinking = C_thinkingPhilsImpl; return phils; } __code putdown_rfork(struct PhilsImpl* phils, __code next(...)) { struct AtomicT_int* right_fork = phils->Rightfork; goto right_fork->set(-1, putdown_lfork); } __code putdown_lfork(struct PhilsImpl* phils, __code next(...)) { struct AtomicT_int* left_fork = phils->Leftfork; goto left_fork->set(-1, thinking); } __code thinking(struct PhilsImpl* phils, struct Fork* fork, __code next(...)) { printf("%d: thinking\n", phils->self); goto pickup_lfork(); } __code pickup_rfork(struct PhilsImpl* phils, __code next(...)) { struct AtomicT_int* right_fork = phils->Rightfork; goto right_fork->checkAndSet(-1, phils->self, pickup_lfork, pickup_rfork); } __code pickup_lfork(struct PhilsImpl* phils, __code next(...)) { struct AtomicT_int* left_fork = phils->Leftfork; goto left_fork->checkAndSet(-1, phils->self, pickup_rfork, eating); } __code eating(struct PhilsImpl* phils, __code next(...)) { printf("%d: eating\n", phils->self); goto putdown_rfork(); }