1+ #include < atomic>
2+ #include < condition_variable>
3+ #include < cstring>
4+ #include < mutex>
5+
6+ #include " ../specs/queue.h"
7+ #include " runtime/include/verifying.h"
8+
9+ constexpr int THREAD_COUNT = 2 ;
10+ constexpr int N = 5 ;
11+
12+ namespace spec {
13+ struct BufferedChannel {
14+ int Send (int v) {
15+ deq.push_back (v);
16+ return 0 ;
17+ }
18+
19+ int TryRecv () {
20+ if (deq.empty ()) {
21+ return -1 ;
22+ }
23+ auto value = deq.front ();
24+ deq.pop_front ();
25+ return value;
26+ }
27+
28+ using method_t = std::function<int (BufferedChannel *l, void *args)>;
29+ static auto GetMethods () {
30+ method_t send_func = [](BufferedChannel *l, void *args) -> int {
31+ auto real_args = reinterpret_cast <std::tuple<int > *>(args);
32+ return l->Send (std::get<0 >(*real_args));
33+ };
34+
35+ method_t try_recv_func = [](BufferedChannel *l, void *args) -> int {
36+ return l->TryRecv ();
37+ };
38+
39+ return std::map<std::string, method_t >{
40+ {" Send"
41+ {" TryRecv"
42+ };
43+ }
44+
45+ std::deque<int > deq;
46+ };
47+
48+ struct BufferedChannelHash {
49+ size_t operator ()(const BufferedChannel &r) const {
50+ int res = 0 ;
51+ for (int elem : r.deq ) {
52+ res += elem;
53+ }
54+ return res;
55+ }
56+ };
57+
58+ struct BufferedChannelEquals {
59+ bool operator ()(const BufferedChannel &lhs,
60+ const BufferedChannel &rhs) const {
61+ return lhs.deq == rhs.deq ;
62+ }
63+ };
64+ }; // namespace spec
65+
66+ struct BufferedChannelVerifier {
67+ bool Verify (CreatedTaskMetaData ctask) {
68+ auto [taskName, is_new, thread_id] = ctask;
69+ debug (stderr, " validating method %s, thread_id: %zu\n " data (),
70+ thread_id);
71+ if (!is_new) {
72+ return true ;
73+ }
74+ if (taskName == " Send"
75+ return size_ + THREAD_COUNT < N;
76+ } else if (taskName == " TryRecv"
77+ return true ;
78+ } else {
79+ assert (false );
80+ }
81+ }
82+
83+ void OnFinished (TaskWithMetaData ctask) {
84+ auto [task, is_new, thread_id] = ctask;
85+ auto taskName = task->GetName ();
86+ if (taskName == " Send"
87+ ++size_;
88+ } else if (taskName == " TryRecv"
89+ if (size_ > 0 ) {
90+ --size_;
91+ }
92+ } else {
93+ assert (false );
94+ }
95+ debug (stderr, " On finished method %s, thread_id: %zu, size: %zu\n "
96+ taskName.data (), thread_id, size_);
97+ }
98+
99+ std::optional<std::string> ReleaseTask (size_t thread_id) {
100+ if (size_ > 0 ) {
101+ return {" TryRecv"
102+ }
103+ return std::nullopt ;
104+ }
105+
106+ size_t size_;
107+ };
108+
109+ struct BufferedChannel {
110+ non_atomic int Send (int v) {
111+ std::unique_lock lock{mutex_};
112+ while (!closed_ && full_) {
113+ send_side_cv_.wait (lock);
114+ }
115+
116+ queue_[sidx_] = v;
117+ sidx_ = (sidx_ + 1 ) % N;
118+ full_ = (sidx_ == ridx_);
119+ empty_ = false ;
120+ return 0 ;
121+ }
122+
123+ // TryRecv is not blocking otherwise it is dual structure
124+ non_atomic int TryRecv () {
125+ std::unique_lock lock{mutex_};
126+ if (closed_ || empty_) {
127+ return -1 ;
128+ }
129+ auto val = queue_[ridx_];
130+ ridx_ = (ridx_ + 1 ) % 5 ;
131+ empty_ = (sidx_ == ridx_);
132+ full_ = false ;
133+ send_side_cv_.notify_one ();
134+ return val;
135+ }
136+
137+ non_atomic int Close () {
138+ closed_.store (true );
139+ send_side_cv_.notify_all ();
140+ return 0 ;
141+ }
142+
143+ std::mutex mutex_;
144+ std::condition_variable send_side_cv_;
145+ std::atomic_bool closed_{false };
146+
147+ bool full_{false };
148+ bool empty_{true };
149+
150+ uint32_t sidx_{0 }, ridx_{0 };
151+
152+ std::array<int , N> queue_{};
153+ };
154+
155+ auto generateInt (size_t ) {
156+ return ltest::generators::makeSingleArg (rand () % 10 + 1 );
157+ }
158+
159+ using spec_t =
160+ ltest::Spec<BufferedChannel, spec::BufferedChannel,
161+ spec::BufferedChannelHash, spec::BufferedChannelEquals>;
162+
163+ LTEST_ENTRYPOINT_CONSTRAINT (spec_t , BufferedChannelVerifier);
164+
165+ target_method (generateInt, void , BufferedChannel, Send, int );
166+ target_method (ltest::generators::genEmpty, int , BufferedChannel, TryRecv);
167+ // target_method(ltest::generators::genEmpty, int, BufferedChannel, Close);
0 commit comments