Skip to content

Commit e785f08

Browse files
committed
extend buffered channel test
1 parent 10b8e07 commit e785f08

File tree

6 files changed

+43
-37
lines changed

6 files changed

+43
-37
lines changed

Dockerfile

Lines changed: 8 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,10 @@
11
FROM silkeh/clang:19 AS ltest
22

3-
RUN apt update && apt install -y git ninja-build valgrind libboost-context-dev libgflags-dev libstdc++-11-dev libclang-19-dev
3+
RUN apt update && apt install -y git ninja-build valgrind libgflags-dev libstdc++-11-dev libclang-19-dev
44
RUN mv /usr/lib/gcc/x86_64-linux-gnu/12 /usr/lib/gcc/x86_64-linux-gnu/_12
55

66
FROM ltest as blocking
7-
RUN apt install -y pkg-config libcapstone-dev && \
7+
RUN apt install -y pkg-config libcapstone-dev libboost-context-dev && \
88
git clone https://github.com/Kirillog/syscall_intercept.git && \
99
cmake syscall_intercept -G Ninja -B syscall_intercept/build -DCMAKE_INSTALL_PREFIX=/usr -DCMAKE_BUILD_TYPE=Release -DCMAKE_C_COMPILER=clang && \
1010
cmake --build syscall_intercept/build --target install
@@ -15,6 +15,12 @@ RUN apt install -y libboost-filesystem-dev libboost-program-options-dev libboost
1515
git clone https://github.com/Kirillog/folly.git && \
1616
cmake folly -G Ninja -B folly/build_dir -DCMAKE_BUILD_TYPE=Release
1717
# cmake --build folly/build_dir --target install
18+
FROM ltest as userver-blocking
19+
# userver conflicts with default libboost-context-dev (1.74) version, 1.81 required
20+
RUN apt install -y python3-dev python3-venv \
21+
libboost-context1.81-dev libboost-filesystem1.81-dev libboost-program-options1.81-dev libboost-regex1.81-dev
22+
libboost-stacktrace1.81-dev libboost-locale1.81-dev \
23+
libzstd-dev libyaml-cpp-dev libcrypto++-dev libnghttp2-dev libev-dev
1824
RUN sh -c "$(wget -O- https://github.com/deluan/zsh-in-docker/releases/download/v1.2.1/zsh-in-docker.sh)" -- \
1925
-p git
2026
CMD [ "zsh" ]

runtime/CMakeLists.txt

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,7 @@ set (SOURCE_FILES
1313
)
1414

1515
add_library(runtime SHARED ${SOURCE_FILES})
16-
find_package(Boost 1.74.0 REQUIRED COMPONENTS context)
16+
find_package(Boost REQUIRED COMPONENTS context)
1717
target_include_directories(runtime PRIVATE include ${Boost_INCLUDE_DIRS})
1818
target_link_libraries(runtime PRIVATE gflags ${Boost_LIBRARIES})
1919
target_link_options(runtime PRIVATE ${CMAKE_ASAN_FLAGS})

runtime/include/pct_strategy.h

Lines changed: 4 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -17,14 +17,7 @@ struct PctStrategy : public BaseStrategyWithThreads<TargetObj, Verifier> {
1717
: BaseStrategyWithThreads<TargetObj, Verifier>(threads_count, ctrs),
1818
current_depth(1),
1919
current_schedule_length(0) {
20-
// We have information about potential number of resumes
21-
// but because of the implementation, it's only available in the task.
22-
// In fact, it doesn't depend on the task, it only depends on the
23-
// constructor
24-
size_t avg_k = 0;
25-
avg_k = avg_k / this->constructors.size();
26-
27-
PrepareForDepth(current_depth, avg_k);
20+
PrepareForDepth(current_depth, 1);
2821
}
2922

3023
std::optional<size_t> NextThreadId() override {
@@ -36,9 +29,9 @@ struct PctStrategy : public BaseStrategyWithThreads<TargetObj, Verifier> {
3629
// Ignore waiting tasks
3730
// debug(stderr, "prior: %d, number %d\n", priorities[i], i);
3831
if (!threads[i].empty() && threads[i].back()->IsBlocked()) {
39-
// debug(stderr, "blocked on %p val %d\n",
40-
// threads[i].back()->GetBlockState().addr,
41-
// threads[i].back()->GetBlockState().value);
32+
debug(stderr, "blocked on %p val %d\n",
33+
threads[i].back()->GetBlockState().addr,
34+
threads[i].back()->GetBlockState().value);
4235
// dual waiting if request finished, but follow up isn't
4336
// skip dual tasks that already have finished the request
4437
// section(follow-up will be executed in another task, so we can't

runtime/include/scheduler.h

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -259,7 +259,6 @@ struct BaseStrategyWithThreads : public Strategy {
259259
constructor.Build(this->state.get(), thread_index, task_index);
260260
auto verified = this->sched_checker.Verify(
261261
std::string(task->GetName()), thread_index);
262-
assert(verified && "wrong release task at termination");
263262
thread.emplace_back(task);
264263
}
265264
}

verifying/blocking/buffered_channel.cpp

Lines changed: 17 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -16,7 +16,7 @@ struct BufferedChannel {
1616
return 0;
1717
}
1818

19-
int TryRecv() {
19+
int Recv() {
2020
if (deq.empty()) {
2121
return -1;
2222
}
@@ -32,13 +32,13 @@ struct BufferedChannel {
3232
return l->Send(std::get<0>(*real_args));
3333
};
3434

35-
method_t try_recv_func = [](BufferedChannel *l, void *args) -> int {
36-
return l->TryRecv();
35+
method_t recv_func = [](BufferedChannel *l, void *args) -> int {
36+
return l->Recv();
3737
};
3838

3939
return std::map<std::string, method_t>{
4040
{"Send", send_func},
41-
{"TryRecv", try_recv_func},
41+
{"Recv", recv_func},
4242
};
4343
}
4444

@@ -67,7 +67,7 @@ struct BufferedChannel {
6767
non_atomic int Send(int v) {
6868
std::unique_lock lock{mutex_};
6969
while (!closed_ && full_) {
70-
debug(stderr, "Waiting...\n");
70+
debug(stderr, "Waiting in send...\n");
7171
send_side_cv_.wait(lock);
7272
}
7373
debug(stderr, "Send\n");
@@ -76,15 +76,17 @@ struct BufferedChannel {
7676
sidx_ = (sidx_ + 1) % N;
7777
full_ = (sidx_ == ridx_);
7878
empty_ = false;
79+
recv_side_cv_.notify_one();
7980
return 0;
8081
}
8182

82-
// TryRecv is not blocking otherwise it is dual structure
83-
non_atomic int TryRecv() {
84-
std::lock_guard lock{mutex_};
85-
if (closed_ || empty_) {
86-
return -1;
83+
non_atomic int Recv() {
84+
std::unique_lock lock{mutex_};
85+
while (!closed_ && empty_) {
86+
debug(stderr, "Waiting in recv...\n");
87+
recv_side_cv_.wait(lock);
8788
}
89+
debug(stderr, "Recv\n");
8890
auto val = queue_[ridx_];
8991
ridx_ = (ridx_ + 1) % 5;
9092
empty_ = (sidx_ == ridx_);
@@ -93,15 +95,16 @@ struct BufferedChannel {
9395
return val;
9496
}
9597

96-
non_atomic int Close() {
98+
int Close() {
9799
closed_.store(true);
98100
send_side_cv_.notify_all();
101+
recv_side_cv_.notify_all();
99102
return 0;
100103
}
101104

102105
std::mutex mutex_;
103-
std::condition_variable send_side_cv_;
104-
std::atomic_bool closed_{false};
106+
std::condition_variable send_side_cv_, recv_side_cv_;
107+
std::atomic<bool> closed_{false};
105108

106109
bool full_{false};
107110
bool empty_{true};
@@ -122,5 +125,4 @@ using spec_t =
122125
LTEST_ENTRYPOINT_CONSTRAINT(spec_t, spec::BufferedChannelVerifier);
123126

124127
target_method(generateInt, void, BufferedChannel, Send, int);
125-
target_method(ltest::generators::genEmpty, int, BufferedChannel, TryRecv);
126-
// target_method(ltest::generators::genEmpty, int, BufferedChannel, Close);
128+
target_method(ltest::generators::genEmpty, int, BufferedChannel, Recv);

verifying/blocking/verifiers/buffered_channel_verifier.h

Lines changed: 13 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -12,11 +12,15 @@ struct BufferedChannelVerifier {
1212
return true;
1313
}
1414
return false;
15-
} else if (task_name == "TryRecv") {
16-
if (size_ > 0) {
17-
--size_;
15+
} else if (task_name == "Recv") {
16+
if (receivers_ == 0) {
17+
++receivers_;
18+
if (size_ > 0) {
19+
--size_;
20+
}
21+
return true;
1822
}
19-
return true;
23+
return false;
2024
} else {
2125
assert(false);
2226
}
@@ -27,21 +31,23 @@ struct BufferedChannelVerifier {
2731
if (task_name == "Send") {
2832
--senders_;
2933
return;
30-
} else if (task_name == "TryRecv") {
34+
} else if (task_name == "Recv") {
35+
--receivers_;
3136
return;
3237
} else {
3338
assert(false);
3439
}
3540
}
3641

3742
std::optional<std::string> ReleaseTask(size_t thread_id) {
38-
if (size_ > 0) {
39-
return {"TryRecv"};
43+
if (senders_ > 0) {
44+
return {"Recv"};
4045
}
4146
return std::nullopt;
4247
}
4348

4449
size_t senders_;
50+
size_t receivers_;
4551
size_t size_;
4652
};
4753
} // namespace spec

0 commit comments

Comments
 (0)