Skip to content

Commit

Permalink
Release GenMC v0.10.0
Browse files Browse the repository at this point in the history
Signed-off-by: Michalis Kokologiannakis <[email protected]>
  • Loading branch information
michaliskok committed Oct 25, 2023
1 parent b5e7340 commit eab70f8
Show file tree
Hide file tree
Showing 2,547 changed files with 26,398 additions and 13,388 deletions.
26 changes: 26 additions & 0 deletions .clang-tidy
Original file line number Diff line number Diff line change
@@ -0,0 +1,26 @@
Checks: |
-*,
clang-analyzer-*,
clang-diagnostic-*,
concurrency-*,
cppcoreguidelines-*,
llvm-*,
-llvmlibc-restrict-system-libc-headers,
-llvm-header-guard,
misc-*,
-misc-non-private-member-variables-in-classes,
-misc-no-recursion,
-misc-use-anonymous-namespace,
readability-*,
-readability-braces-around-statements,
modernize-*,
performance-*,
CheckOptions:
- key: readability-function-cognitive-complexity.IgnoreMacros
value: true
- key: readability-identifier-length.IgnoredVariableNames
value: 'i|g|e|EE|l|r|s|w|f|b|br|v|hb'
- key: readability-identifier-length.IgnoredLoopCounterNames
value: 'i|j|k|g|e|EE|l|r|s|w|f|b|br|v|hb'
- key: readability-identifier-length.IgnoredParameterNames
value: 'g|e|EE|l|r|s|w|f|b|br|v|hb'
31 changes: 12 additions & 19 deletions .gitignore
Original file line number Diff line number Diff line change
Expand Up @@ -5,29 +5,20 @@ genmc
*.bak
*.backup
.*.sw[a-z]
.cache
.deps
*.dirstamp
compile_commands.json

*.aux
*.bbl
*.blg
*.fdb_latexmk
*.fls
*.log
*.toc
*.xdv
*.tex
*.out

*.ll
*.gcno

*.annot
*.cmo
*.cma
*.cmi
*.a
*.o
*.cmx
*.cmxs
*.cmxa

*.ll
*.out

doc/doxygen

Makefile
Makefile.in
Expand All @@ -45,3 +36,5 @@ depcomp
install-sh
missing
stamp-*
ylwrap
test-driver
38 changes: 38 additions & 0 deletions CHANGELOG.md
Original file line number Diff line number Diff line change
Expand Up @@ -4,8 +4,41 @@ Notable changes to GenMC will be documented in this file. This
repository is only updated whenever a new version of GenMC is
released.


## [Unreleased]

- Documentation


## [0.10.0] - 2023.10.25
### Added

- Support for SC, TSO, RA memory models
- Symmetry reduction (automatic or via `__VERIFIER_spawn_symmetric`)
- In-place revisiting (from Awamoche [CAV 2023])
- Preemption/Round-Robin bounding under SC [TACAS 2023, FMCAD 2023]
- State-space size estimation before verification begins
- Performance optimizations
- Support for LLVM-16
- Rudimentary doxygen documentation

### Changed

- GenMC now requires a compiler with C++20 support

### Deprecated

- Support for LLVM-{7,8,9}

### Removed

- Support for LKMM, Persevere

### Fixes

- Various bug issues


## [0.9] - 2022.12.26
### Added

Expand All @@ -27,6 +60,7 @@ released.

- Bug fixes


## [0.8] - 2022.02.22
### Added

Expand Down Expand Up @@ -110,6 +144,7 @@ released.
- Proper support for `pthread_mutex_init` and `pthread_mutex_destroy`
- Various bugs


## [0.5.3] - 2020.12.06
### Added

Expand All @@ -122,11 +157,13 @@ released.
- Documentation fix and update
- Other minor bugs


## [0.5.2] - 2020.10.08
### Added

- Documentation for Persevere, LAPOR


## [0.5.1] - 2020.10.01
### Added

Expand All @@ -140,6 +177,7 @@ released.

- Build fixes for LLVM 10


## [0.5] - 2020.09.23
### Added

Expand Down
137 changes: 123 additions & 14 deletions Makefile.am
Original file line number Diff line number Diff line change
@@ -1,18 +1,127 @@
SUBDIRS = src include
# where to install the headers on the system
genmcdir = $(pkgincludedir)

.PHONY: test ftest
test:
$(MAKE) -C src
cd $(top_builddir)/scripts && ./driver.sh --debug
# the list of header files that belong to the library
nobase_genmc_HEADERS = \
include/assert.h \
include/atomic \
include/bits/stat.h \
include/cassert \
include/errno.h \
include/fcntl.h \
include/genmc.h \
include/genmc_internal.h \
include/lkmm.h \
include/pthread.h \
include/stdatomic.h \
include/stdio.h \
include/stdlib.h \
include/sys/stat.h \
include/sys/types.h \
include/thread \
include/threads.h \
include/unistd.h

ftest:
$(MAKE) -C src
cd $(top_builddir)/scripts && ./driver.sh --fast --debug
noinst_LIBRARIES = libgenmc.a
libgenmc_a_SOURCES = \
src/ASize.cpp src/ASize.hpp \
src/BisimilarityCheckerPass.cpp src/BisimilarityCheckerPass.hpp \
src/Bitmask.hpp \
src/BoundDecider.cpp src/BoundDecider.hpp \
src/CallInfoCollectionPass.cpp src/CallInfoCollectionPass.hpp \
src/CodeCondenserPass.cpp src/CodeCondenserPass.hpp \
src/ContextBoundDecider.cpp src/ContextBoundDecider.hpp \
src/Calculator.hpp \
src/CallInstWrapper.hpp \
src/ConfirmationAnnotationPass.cpp src/ConfirmationAnnotationPass.hpp \
src/Config.cpp src/Config.hpp \
src/DeclareInternalsPass.cpp src/DeclareInternalsPass.hpp \
src/DefineLibcFunsPass.cpp src/DefineLibcFunsPass.hpp \
src/DepExecutionGraph.cpp src/DepExecutionGraph.hpp \
src/DepInfo.cpp src/DepInfo.hpp \
src/DepTracker.hpp \
src/DepView.cpp src/DepView.hpp \
src/DriverFactory.hpp \
src/EliminateAnnotationsPass.cpp src/EliminateAnnotationsPass.hpp \
src/EliminateCASPHIsPass.cpp src/EliminateCASPHIsPass.hpp \
src/EliminateCastsPass.cpp src/EliminateCastsPass.hpp \
src/EliminateRedundantInstPass.cpp src/EliminateRedundantInstPass.hpp \
src/EliminateUnusedCodePass.cpp src/EliminateUnusedCodePass.hpp \
src/Error.hpp \
src/EscapeCheckerPass.cpp src/EscapeCheckerPass.hpp \
src/Event.cpp src/Event.hpp \
src/EventAttr.hpp \
src/EventLabel.cpp src/EventLabel.hpp \
src/Execution.cpp \
src/ExecutionGraph.cpp src/ExecutionGraph.hpp \
src/ExternalFunctions.cpp \
src/FunctionInlinerPass.cpp src/FunctionInlinerPass.hpp \
src/GenMCDriver.cpp src/GenMCDriver.hpp \
src/GraphIterators.hpp \
src/IMMDriver.cpp src/IMMDriver.hpp \
src/InstAnnotator.cpp src/InstAnnotator.hpp \
src/Interpreter.cpp Interpreter.h \
src/InterpreterEnumAPI.cpp src/InterpreterEnumAPI.hpp \
src/IntrinsicLoweringPass.cpp src/IntrinsicLoweringPass.hpp \
src/LabelVisitor.hpp \
src/LoadAnnotationPass.cpp src/LoadAnnotationPass.hpp \
src/LocalSimplifyCFGPass.cpp src/LocalSimplifyCFGPass.hpp \
src/Logger.hpp \
src/LLVMModule.cpp src/LLVMModule.hpp \
src/LLVMUtils.cpp src/LLVMUtils.hpp \
src/LoopUnrollPass.cpp src/LoopUnrollPass.hpp \
src/LoopJumpThreadingPass.cpp src/LoopJumpThreadingPass.hpp \
src/Matrix2D.hpp Matrix2D.tcc \
src/MaximalIterator.hpp \
src/MDataCollectionPass.hpp src/MDataCollectionPass.cpp \
src/MemAccess.hpp \
src/MMDetectorPass.cpp src/MMDetectorPass.hpp \
src/ModuleID.hpp \
src/ModuleInfo.cpp src/ModuleInfo.hpp \
src/NameInfo.cpp src/NameInfo.hpp \
src/Parser.cpp src/Parser.hpp \
src/PromoteMemIntrinsicPass.cpp src/PromoteMemIntrinsicPass.hpp \
src/PropagateAssumesPass.cpp src/PropagateAssumesPass.hpp \
src/RADriver.cpp src/RADriver.hpp \
src/RC11Driver.cpp src/RC11Driver.hpp \
src/Revisit.cpp src/Revisit.hpp \
src/RoundBoundDecider.cpp src/RoundBoundDecider.hpp \
src/SAddr.cpp src/SAddr.hpp \
src/SAddrAllocator.hpp \
src/SCDriver.cpp src/SCDriver.hpp \
src/SExpr.tcc src/SExpr.hpp \
src/SExprVisitor.tcc src/SExprVisitor.hpp \
src/Stamp.cpp src/Stamp.hpp \
src/SVal.cpp src/SVal.hpp \
src/SpinAssumePass.cpp src/SpinAssumePass.hpp \
src/WBIterator.hpp \
src/ThreadInfo.hpp \
src/ThreadPinner.cpp src/ThreadPinner.hpp \
src/ThreadPool.cpp src/ThreadPool.hpp \
src/TSODriver.cpp src/TSODriver.hpp \
src/WorkSet.hpp src/WorkSet.cpp \
src/value_ptr.hpp \
src/Verbosity.hpp src/Verbosity.cpp \
src/VectorClock.hpp src/VectorClock.cpp \
src/VerificationError.hpp src/VerificationError.cpp \
src/View.hpp src/View.cpp \
src/VSet.hpp src/VSet.tcc

ctest:
$(MAKE) -C src
cd $(top_builddir)/scripts && ./driver.sh --fast
TESTS=scripts/fast-driver.sh scripts/randomize-driver.sh

rtest:
$(MAKE) -C src
cd $(top_builddir)/scripts && ./randomize-driver.sh
AM_CXXFLAGS = -DINCLUDE_DIR=\"$(pkgincludedir)/$(pkg)\" -DSRC_INCLUDE_DIR=\"$(abs_top_srcdir)/include\" $(COVERAGE_CXXFLAGS)
bin_PROGRAMS = genmc
genmc_SOURCES = src/main.cpp
genmc_LDADD = libgenmc.a -lpthread $(COVERAGE_LDFLAGS)

include Makefile.am.coverage

@DX_RULES@
MOSTLYCLEANFILES = DX_CLEANFILES

if LINT
lint-local: $(libgenmc_a_SOURCES) $(genmc_SOURCES)
-$(CPPLINT) -header-filter='^(?!llvm/).+' -config-file='$(top_srcdir)/.clang-tidy' $^

check-local: lint-local
endif
27 changes: 27 additions & 0 deletions Makefile.am.coverage
Original file line number Diff line number Diff line change
@@ -0,0 +1,27 @@
# Coverage targets

if HAVE_GCOV

.PHONY: clean-gcda
clean-gcda:
@echo Removing old coverage results
-find -name '*.gcda' -print | xargs -r rm

.PHONY: coverage-html generate-coverage-html clean-coverage-html
coverage-html: clean-gcda
-$(MAKE) $(AM_MAKEFLAGS) -k check
$(MAKE) $(AM_MAKEFLAGS) generate-coverage-html

generate-coverage-html:
@echo Collecting coverage data
$(LCOV) --directory $(top_builddir) --capture --output-file coverage.info --no-checksum --compat-libtool
$(LCOV) -r coverage.info "/usr*" -o coverage.info
LANG=C $(GENHTML) --prefix $(top_builddir) --output-directory coveragereport --title "Code Coverage" --legend --show-details coverage.info

clean-coverage-html: clean-gcda
-$(LCOV) --directory $(top_builddir) -z
-rm -rf coverage.info coveragereport

clean-local: clean-coverage-html

endif # HAVE_GCOV
15 changes: 8 additions & 7 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -31,13 +31,14 @@ please issue the following command:

#### Dependencies

You will need a C++14-compliant compiler and an LLVM installation.
You will need a C++20-compliant compiler and an LLVM installation.
The LLVM versions currently supported are:
7.0.1, 8.0.1, 9.0.1, 10.0.1, 11.0.0, 12.0.1, 13.0.0, 14.0.0, 15.0.0.
10.0.1, 11.0.0, 12.0.1, 13.0.0, 14.0.0, 15.0.0, 16.0.0 (deprecated:
7.0.1, 8.0.1, 9.0.1).

##### GNU/Linux

In order to use the tool on a Debian-based installation, you will need the
In order to use the tool on a Debian-based installation, you need the
following packages:

autoconf automake clang llvm llvm-dev libffi-dev
Expand All @@ -59,7 +60,7 @@ For a default build issue:
./configure
make

This will leave the `genmc` executable in the `src` directory.
This will leave the `genmc` executable in the build directory.
You can either run it from there (as in the examples below), or issue
`make install`.

Expand All @@ -68,7 +69,7 @@ executable in parallel and will also run a subset of all the tests
that come with the system to see if the system was built correctly or
not:

make -j ctest
make -j check

##### Mac OS X

Expand All @@ -83,11 +84,11 @@ For a default build issue:

* To see a list of available options run:

./src/genmc --help
./genmc --help

* To run a particular testcase run:

./src/genmc [options] <file>
./genmc [options] <file>

* For more detailed usage examples please refer to the [manual](doc/manual.pdf).

Expand Down
Loading

0 comments on commit eab70f8

Please sign in to comment.