Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Release v3.6.0 #12

Merged
merged 15 commits into from
May 23, 2024
67 changes: 67 additions & 0 deletions .cmake-format
Original file line number Diff line number Diff line change
@@ -0,0 +1,67 @@
{
"parse": {
"additional_commands": {
"add_toolchain": {
"pargs": {
"nargs": 3
}
},
"add_vsyncer_check": {
"kwargs": {
"CFLAGS": "+",
"DEPENDENCIES": "+",
"MEMORY_MODELS": "+",
"SOURCE": 1,
"TARGET": 1,
"TIMEOUT": 1
},
"pargs": {
"flags": [],
"nargs": "*"
}
},
"get_filename_wext": {
"pargs": {
"nargs": 2
}
},
"get_git_tag": {
"pargs": {
"nargs": 1
}
},
"get_includes": {
"pargs": {
"nargs": 1
}
},
"get_toolkit_qemu": {
"pargs": {
"nargs": 3
}
},
"project_tag": {
"pargs": {
"nargs": 0
}
},
"CPMAddPackage": {},
"_CPMAddPackage": {},
"vsync_install": {
"kwargs": {
"DIRECTORY": "+",
"DESTINATION": "+",
"COMPONENTS": "+",
"EXTRA_ARGS": "+"
},
"pargs": {
"flags": [],
"nargs": "*"
}
}
}
},
"format": {
"tab_size": 4
}
}
7 changes: 5 additions & 2 deletions .github/workflows/actions.yml
Original file line number Diff line number Diff line change
Expand Up @@ -23,14 +23,17 @@ jobs:
container: ghcr.io/open-s4c/vsyncer-ci:sha-5f9eab426f2608a9fac2eabf15c7614c73a81736
strategy:
matrix:
test-dir: [ {p: "test", c: "spinlock"}, {p: "test", c: "quack"}, {p: "test", c: "queue"}, {p: "verify", c: "unbounded_queue"}, {p: "verify", c: "listset"} ]
test-dir: [ {p: "test", c: "spinlock"}, {p: "test", c: "quack"}, {p: "test", c: "queue"},
{p: "verify", c: "unbounded_queue"}, {p: "verify", c: "listset"} ,
{p: "verify", c: "stack"}, {p: "verify", c: "thread"}, {p: "verify", c: "simpleht"},
{p: "verify", c: "bitmap"}, {p: "verify", c: "treeset"}]
steps:
- name: Print vsyncer version
run: vsyncer version
- name: Check out repository code
uses: actions/checkout@v4
- name: Configure Verification
run: cmake -S. -Bbuild -DVSYNCER_CHECK=ON
run: cmake -S. -Bbuild -DVSYNCER_CHECK=ON -DVSYNCER_CHECK_FULL=OFF
- name: Build Verification Clients for ${{ matrix.test-dir }}
run: cmake --build build/${{ matrix.test-dir.p }}/${{ matrix.test-dir.c }}
- name: Run Verification
Expand Down
19 changes: 19 additions & 0 deletions CHANGELOG.md
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,25 @@ is not guaranteed to result in increment of major version.
Please note that the version correlates to the internal libvsync, which is a superset of
what exists in open-s4c libvsync.


### [3.6.0]

### Added

- cnalock, clhlock, arraylock, twalock, hmcslock, hclhlock, rec_seqlock and hemlock
- bitmap
- simpleht hashtable
- elimination and xbo backoff stacks
- mutex, cond, and once
- treeset

### Fixed

- implementation of `rwlock_acquired_by_readers`, which used to return
true also in the case of neither a writer nor a reader acquired the lock.
Now it returns true if and only if the lock is acquired by readers, as the name suggests.


### [3.5.0]

### Added
Expand Down
51 changes: 32 additions & 19 deletions CMakeLists.txt
Original file line number Diff line number Diff line change
Expand Up @@ -3,11 +3,14 @@ cmake_minimum_required(VERSION 3.16)
project(
libvsync
LANGUAGES C
VERSION 3.5.0
DESCRIPTION "Verified library of atomics, synchronization primitives and concurrent data structures")
VERSION 0.0.0
lilith218 marked this conversation as resolved.
Show resolved Hide resolved
DESCRIPTION
"Verified library of atomics, synchronization primitives and concurrent data structures"
)

option(LIBVSYNC_ADDRESS_SANITIZER "Compile with -fsanitize=address" "off")
option(LIBVSYNC_CODECHECK_BINSCOPE "Compile with necessary flags for binscope" "off")
option(LIBVSYNC_CODECHECK_BINSCOPE "Compile with necessary flags for binscope"
"off")

include(GNUInstallDirs)
include(cmake/export.cmake)
Expand All @@ -23,9 +26,9 @@ install(DIRECTORY include/vsync DESTINATION include)
install(FILES vmm/vmm.cat DESTINATION share/vsync)
install(TARGETS vsync EXPORT ${PROJECT_TARGETS})

##############################################################
# Check for memset_s memcpy_s existence
##############################################################
# ##############################################################################
# Check for memset_s memcpy_s existence
# ##############################################################################
check_symbol_exists(memset_s "string.h" VSYNC_MEMSET_S_EXISTS)
if(VSYNC_MEMSET_S_EXISTS)
target_compile_definitions(vsync INTERFACE "VSYNC_MEMSET_S_EXISTS")
Expand All @@ -36,20 +39,29 @@ if(VSYNC_MEMCPY_S_EXISTS)
endif()

if(CMAKE_PROJECT_NAME STREQUAL PROJECT_NAME)
##############################################################
# Important Config must be set
##############################################################
# ##########################################################################
# Important Config must be set
# ##########################################################################
set(ATOMICS_DIR ${PROJECT_SOURCE_DIR})

##############################################################
# Commands
##############################################################
set(FMT_CMD ${PROJECT_SOURCE_DIR}/scripts/clang-format.sh
${CMAKE_SOURCE_DIR})
set(STYLE_FILE ${PROJECT_SOURCE_DIR}/.clang-format)
# ##########################################################################
# Commands
# ##########################################################################
set(CMAKE_FMT_CMD ${PROJECT_SOURCE_DIR}/scripts/cmake-format.sh
${CMAKE_SOURCE_DIR})

add_custom_target(clang-format-apply
COMMAND env STYLE=${STYLE_FILE} SILENT=true ${FMT_CMD})
set(CMAKE_STYLE_FILE ${PROJECT_SOURCE_DIR}/.cmake-format)

add_custom_target(cmake-format-apply COMMAND env STYLE=${CMAKE_STYLE_FILE}
SILENT=true ${CMAKE_FMT_CMD})

set(CLANG_FMT_CMD ${PROJECT_SOURCE_DIR}/scripts/clang-format.sh
${CMAKE_SOURCE_DIR})

set(CLANG_STYLE_FILE ${PROJECT_SOURCE_DIR}/.clang-format)

add_custom_target(clang-format-apply COMMAND env STYLE=${CLANG_STYLE_FILE}
SILENT=true ${CLANG_FMT_CMD})

add_custom_target(
sanitize-vsync
Expand Down Expand Up @@ -77,8 +89,9 @@ if(CMAKE_PROJECT_NAME STREQUAL PROJECT_NAME)
endif()
if(LIBVSYNC_CODECHECK_BINSCOPE)
target_compile_definitions(vsync INTERFACE _FORTIFY_SOURCE=2)
target_compile_options(vsync INTERFACE -fstack-protector-strong -fstack-protector-all -fPIE -fPIC -O2)
target_compile_options(
vsync INTERFACE -fstack-protector-strong -fstack-protector-all
-fPIE -fPIC -O2)
target_link_options(vsync INTERFACE -s -pie -Wl,-z,relro,-z,now)
endif()
endif()

52 changes: 46 additions & 6 deletions cmake/check.cmake
Original file line number Diff line number Diff line change
@@ -1,3 +1,5 @@
option(VSYNCER_CHECK "enable vsyncer checks" off)
option(VSYNCER_CHECK_FULL "disable quick vsyncer checks" off)
function(add_vsyncer_check)
# skip if VSYNCER_CHECK is not defined
if(NOT VSYNCER_CHECK)
Expand Down Expand Up @@ -47,8 +49,12 @@ function(add_vsyncer_check)
CFLAGS #
-I${PROJECT_SOURCE_DIR}/include #
-DVSYNC_VERIFICATION #
-DVSYNC_VERIFICATION_QUICK
-DVSYNC_SMR_NOT_AVAILABLE)
if(VSYNCER_CHECK_FULL)
set(TIMEOUT 3600)
else()
list(APPEND CFLAGS -DVSYNC_VERIFICATION_QUICK)
endif()
# ##########################################################################
# Define mode checker env vars
# ##########################################################################
Expand Down Expand Up @@ -88,12 +94,44 @@ function(add_vsyncer_check)
foreach(WMM IN ITEMS ${WMMS})
set(TEST_NAME ${TARGET}_${WMM})
string(TOUPPER ${WMM} WMM_UP)
list(APPEND CFLAGS -DVSYNC_VERIFICATION_${WMM_UP})
string(REPLACE ";" " " CFLAGS "${CFLAGS}")
string(REPLACE "\"'\"" "\"" CFLAGS "${CFLAGS}")
set(COMPILE_FLAGS ${CFLAGS} -DVSYNC_VERIFICATION_${WMM_UP})

# ######################################################################
# Compile ll file with vsyncer
# ######################################################################

set(VSYNCER_CHECK_LL ${CMAKE_CURRENT_SOURCE_DIR}/${TEST_NAME}.ll)

set(VSYNCER_COMPILE_CMD
env
CFLAGS="${COMPILE_FLAGS}"
vsyncer
compile
-d
--checker
${CHECKER}
-o=${VSYNCER_CHECK_LL}
${CLIENT}
|
tee
${VSYNCER_CHECK_LL}.log
|
grep
-vE
"^# clang")

add_custom_command(
OUTPUT ${VSYNCER_CHECK_LL}
COMMAND ${VSYNCER_COMPILE_CMD}
DEPENDS ${CLIENT})

add_custom_target(${TEST_NAME} ALL DEPENDS ${VSYNCER_CHECK_LL})

# ######################################################################
# Run vsyncer check with ctest on the generated ll file
# ######################################################################
set(VSYNCER_CMD #
env
CFLAGS=${CFLAGS} #
${CHECKER_ENV} #
vsyncer
check
Expand All @@ -106,7 +144,9 @@ function(add_vsyncer_check)
${WMM} #
--timeout
${TIMEOUT}s)
add_test(NAME ${TEST_NAME} COMMAND ${VSYNCER_CMD} ${CLIENT})
add_test(NAME ${TEST_NAME} COMMAND ${VSYNCER_CMD} ${VSYNCER_CHECK_LL})
set_property(TEST ${TEST_NAME} PROPERTY SKIP_RETURN_CODE 1)
math(EXPR CTEST_TIMEOUT "${TIMEOUT} + 5")
set_tests_properties(${TEST_NAME} PROPERTIES TIMEOUT ${CTEST_TIMEOUT})
endforeach()
endfunction()
7 changes: 7 additions & 0 deletions doc/api/vsync/GROUP_linearizable.md
Original file line number Diff line number Diff line change
Expand Up @@ -13,13 +13,20 @@ _Group of algorithms linearizable algorithms._
| [vsync/map/listset_lazy.h](map/listset_lazy.h.md)|This is a partially parallel implementation with lock-free get. | ✔ | ❌ | ✔ | ❌ |
| [vsync/map/listset_lf.h](map/listset_lf.h.md)|Lock-free implementation of listset. | ✔ | ✔ | ✔ | ❌ |
| [vsync/map/listset_opt.h](map/listset_opt.h.md)|This implementation is an optimized verison of listset_fine. | ✔ | ❌ | ✔ | ❌ |
| [vsync/map/simpleht.h](map/simpleht.h.md)|Simple lock-free hashtable. | ✔ | ✔ | ❌ | ❌ |
| [vsync/map/treeset_bst_coarse.h](map/treeset_bst_coarse.h.md)|This implementation of treeset uses unbalanced binary search tree (BST) and coarse-grained locking. | ✔ | ❌ | ❌ | ❌ |
| [vsync/map/treeset_bst_fine.h](map/treeset_bst_fine.h.md)|This implementation of treeset uses unbalanced binary search tree (BST) and fine-grained locking. | ✔ | ❌ | ❌ | ❌ |
| [vsync/map/treeset_rb_coarse.h](map/treeset_rb_coarse.h.md)|This implementation of treeset uses balanced red-black tree (RB) and coarse-grained locking. | ✔ | ❌ | ❌ | ❌ |
| [vsync/map/treeset_rb_fine.h](map/treeset_rb_fine.h.md)|This implementation of treeset uses balanced red-black tree (RB) and fine-grained locking. | ✔ | ❌ | ❌ | ❌ |
| [vsync/queue/bounded_locked.h](queue/bounded_locked.h.md)|Multi-producer, multi-consumer bounded queue protected by a spinlock. | ✔ | ❌ | ❌ | ❌ |
| [vsync/queue/bounded_mpmc.h](queue/bounded_mpmc.h.md)|Lockless, multi-producer, multi-consumer bounded queue. | ✔ | ❌ | ❌ | ❌ |
| [vsync/queue/bounded_spsc.h](queue/bounded_spsc.h.md)|Single-producer, single-consumer, wait-free bounded queue. | ✔ | ✔ | ❌ | ❌ |
| [vsync/queue/unbounded_queue_lf.h](queue/unbounded_queue_lf.h.md)|Lock-free unbounded queue. | ✔ | ✔ | ✔ | ✔ |
| [vsync/queue/unbounded_queue_lf_recycle.h](queue/unbounded_queue_lf_recycle.h.md)|Lock-free recycle unbounded queue. | ✔ | ✔ | ❌ | ✔ |
| [vsync/queue/unbounded_queue_total.h](queue/unbounded_queue_total.h.md)|Unbounded blocking total queue. | ✔ | ❌ | ❌ | ✔ |
| [vsync/stack/elimination_stack.h](stack/elimination_stack.h.md)|Unbounded lock-free stack with elimination backoff. | ✔ | ✔ | ✔ | ❌ |
| [vsync/stack/quack.h](stack/quack.h.md)|Lockfree concurrent stack/queue (Treiber stack) | ✔ | ✔ | ❌ | ❌ |
| [vsync/stack/xbo_stack.h](stack/xbo_stack.h.md)|Unbounded lock-free stack with exponential backoff. | ✔ | ✔ | ✔ | ❌ |


---
3 changes: 3 additions & 0 deletions doc/api/vsync/GROUP_lock_free.md
Original file line number Diff line number Diff line change
Expand Up @@ -9,10 +9,13 @@ _Group of algorithms with lock-free progress condition._
| --- | --- | --- | --- | --- | --- |
| [vsync/map/hashtable_standard.h](map/hashtable_standard.h.md)|This is a lock-free listset based hashtable. | ✔ | ✔ | ✔ | ❌ |
| [vsync/map/listset_lf.h](map/listset_lf.h.md)|Lock-free implementation of listset. | ✔ | ✔ | ✔ | ❌ |
| [vsync/map/simpleht.h](map/simpleht.h.md)|Simple lock-free hashtable. | ✔ | ✔ | ❌ | ❌ |
| [vsync/queue/bounded_spsc.h](queue/bounded_spsc.h.md)|Single-producer, single-consumer, wait-free bounded queue. | ✔ | ✔ | ❌ | ❌ |
| [vsync/queue/unbounded_queue_lf.h](queue/unbounded_queue_lf.h.md)|Lock-free unbounded queue. | ✔ | ✔ | ✔ | ✔ |
| [vsync/queue/unbounded_queue_lf_recycle.h](queue/unbounded_queue_lf_recycle.h.md)|Lock-free recycle unbounded queue. | ✔ | ✔ | ❌ | ✔ |
| [vsync/stack/elimination_stack.h](stack/elimination_stack.h.md)|Unbounded lock-free stack with elimination backoff. | ✔ | ✔ | ✔ | ❌ |
| [vsync/stack/quack.h](stack/quack.h.md)|Lockfree concurrent stack/queue (Treiber stack) | ✔ | ✔ | ❌ | ❌ |
| [vsync/stack/xbo_stack.h](stack/xbo_stack.h.md)|Unbounded lock-free stack with exponential backoff. | ✔ | ✔ | ✔ | ❌ |


---
2 changes: 2 additions & 0 deletions doc/api/vsync/GROUP_requires_smr.md
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,8 @@ Users are expected to couple the usage of these algorithms with an SMR scheme fr
| [vsync/map/listset_lf.h](map/listset_lf.h.md)|Lock-free implementation of listset. | ✔ | ✔ | ✔ | ❌ |
| [vsync/map/listset_opt.h](map/listset_opt.h.md)|This implementation is an optimized verison of listset_fine. | ✔ | ❌ | ✔ | ❌ |
| [vsync/queue/unbounded_queue_lf.h](queue/unbounded_queue_lf.h.md)|Lock-free unbounded queue. | ✔ | ✔ | ✔ | ✔ |
| [vsync/stack/elimination_stack.h](stack/elimination_stack.h.md)|Unbounded lock-free stack with elimination backoff. | ✔ | ✔ | ✔ | ❌ |
| [vsync/stack/xbo_stack.h](stack/xbo_stack.h.md)|Unbounded lock-free stack with exponential backoff. | ✔ | ✔ | ✔ | ❌ |


---
2 changes: 2 additions & 0 deletions doc/api/vsync/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -16,11 +16,13 @@ _libvsync is library of robust atomics, synchronization primitives, concurrent d
| Directory|Description|
| --- | --- |
| [vsync/atomic](atomic/README.md)|Rich interface of atomic operations and fences. |
| [vsync/bitmap](bitmap/README.md)|Bitmap implementations. |
| [vsync/map](map/README.md)|This is a collection of algos that implement map interface. |
| [vsync/queue](queue/README.md)|Queues, priority queues and ringbuffers. |
| [vsync/smr](smr/README.md)|Safe Memory Reclamation Schemes. |
| [vsync/spinlock](spinlock/README.md)|Spinlocks for kernel and userspace. |
| [vsync/stack](stack/README.md)|Concurrent stacks. |
| [vsync/thread](thread/README.md)|Userspace synchronization primitives. |


---
6 changes: 3 additions & 3 deletions doc/api/vsync/atomic/await.h.md
Original file line number Diff line number Diff line change
Expand Up @@ -40,12 +40,12 @@ node_t *next = vatomicptr_await_neq_acq(me->next, NULL);



The following example waits for the pointer me->next to be equal to pred. Once the condition is met, write NULL in me->next. The variable next contains the value that satisfied the condition. The operation has an release barrier.
The following example waits for the pointer me->next to be equal to pred. Once the condition is met, write NULL in me->next. The variable next contains the value that satisfied the condition. The operation has a release barrier.



```
node_t *next = vatomicptr_await_eq_set_acq(me->next, pred, NULL);
```c
node_t *next = vatomicptr_await_eq_set_rel(me->next, pred, NULL);
```


Expand Down
13 changes: 13 additions & 0 deletions doc/api/vsync/bitmap/README.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,13 @@
# [vsync](../README.md) / bitmap
_Bitmap implementations._

---
## File Index


| File|Description|
| --- | --- |
| [vsync/bitmap/bitmap.h](bitmap.h.md)|A bitmap implementation. |


---
Loading