Update README and LICENSE

Signed-off-by: draco <dracode01@gmail.com>

.github/workflows/docker-image.yml

@@ -2,9 +2,11 @@ name: Docker Image CI
 
 on:
   push:
-    branches: [ "main", "dev-ui" ]
+    branches:
+      - '*'
   pull_request:
-    branches: [ "main" ]
+    branches:
+      - '*'
 
 env:
   REGISTRY: ghcr.io

LICENSE

@@ -0,0 +1,21 @@
+MIT License
+
+Copyright (c) 2024 dracoooooo
+
+Permission is hereby granted, free of charge, to any person obtaining a copy
+of this software and associated documentation files (the "Software"), to deal
+in the Software without restriction, including without limitation the rights
+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all
+copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+SOFTWARE.

README.md

@@ -1,134 +1,100 @@
-# DBTest
+# IsoVista
 
-i18n: [中文版](README_zh.md)
+IsoVista is a black-box isolation checking system for databases that supports various isolation levels, ensures accurate and efficient bug detection, provides clear bug visualizations, and offers benchmarking for performance analysis. 
+It is designed to comprehensively test and verify the isolation guarantees of databases, helping developers to find and fix issues more effectively.
 
-DBTest is a platform designed for black-box testing of database transaction isolation levels. By integrating various testing methods for isolation levels, it allows convenient and efficient testing of different databases. It also supports performance analysis of the testing methods. In summary, DBTest offers high scalability and excellent usability.
+## Architecture
 
-The general architecture of this platform is as follows:
+![arch](images/arch.png)
 
-![framework](framework.png)
+## Key Features
 
-# Support
+- **Support for Multiple Isolation Levels**: IsoVista is capable of checking a wide spectrum of isolation levels, including read committed (RC), repeatable read (RR), read atomicity (RA), transactional causal consistency (TCC), snapshot isolation (SI) and serializability (SER). 
 
-## Databases
+- **Complete and Efficient Checking**: IsoVista is built upon sound and complete formal characterizations of all supported isolation levels, which ensures the absence of false positives and the detection of all pertinent bugs in DBMS execution histories. 
+IsoVista enhances checking performance through optimized SMT encoding for stronger isolation levels and efficient data structures for managing transactional dependency graphs in weaker levels.
 
-Currently, the following databases are supported. You can use the docker-compose files in the [scripts/](https://c.binjie.fun/scripts/) directory to quickly deploy the databases for testing (currently supporting single-node database deployment):
+- **Informative Bug Visualization**: Upon detecting an isolation bug, IsoVista provides detailed visualizations of the bug scenario, including the core transactions involved and their dependencies. 
+This feature aids developers in understanding the nature of the bug and facilitates the debugging process.
 
-- MySQL
-- PostgreSQL
-- H2
-
-## Workloads
-
-Currently, the following workloads are supported:
-
-| Workload | Description                                                  |
-| -------- | ------------------------------------------------------------ |
-| GENERAL  | Simulates the workload generated by concurrent access to the database from multiple sessions. Parameters such as the number of simulated sessions, number of transactions per session, number of operations per transaction, read operation ratio, number of workload keys, and distribution type of transaction access keys are randomly generated. |
-| TPCC     | TODO                                                         |
-
-## Consistency Checking Algorithms
+- **Benchmarking and Performance Profiling**: IsoVista includes tools for monitoring runtime information like CPU and memory utilization, and for profiling checking statistics such as time and memory usage across different workloads. 
+These capabilities help developers adjust their checking strategies and explore new optimizations for their tools.
 
-The following consistency checking algorithms and their corresponding isolation levels are currently supported:
+## Support
 
-| Checker | Supported Isolation Levels                             |
-| ------- | ------------------------------------------------------ |
-| C4      | READ_COMMITTED<br>READ_ATOMICITY<br>CAUSAL_CONSISTENCY |
-| PolySI  | SNAPSHOT_ISOLATION                                     |
+### Databases
 
-# How to build
-
-To compile DBTest, the following environments are required:
-
-- JDK 11
-- Maven
-- Git
-
-Execute the following commands to compile the DBTest source code:
+- MySQL
+- PostgreSQL
+- MariaDB
 
-```
-git clone https://github.com/hengxin/db-testing-platform
-cd db-testing-platform
-mvn clean package
-```
+### Isolation Levels
 
-Then you can find the compiled shaded jar file in the target directory.
+- Read Committed
+- Repeatable Read
+- Read Atomicity
+- Transactional Causal Consistency
+- Snapshot Isolation
+- Serializable
 
-# Usage
+### Models
 
-## Parameter Settings
+#### read-write register
 
-As there are many running parameters, all parameters are placed in `config.properties`. Here is a detailed explanation of each running parameter:
+`r/w(key, value, session id, txn id)`
 
-### Database Connection
+Example of history:
 
 ```
-db.url= # JDBC URL
-db.username= # username
-db.password= # password
-db.isolation= # transaction isolation level
-db.type= # database type, supports MYSQL, POSTGRESQL and H2
+w(1,0,0,0)
+w(2,0,0,0)
+w(1,1,1,1)
+r(2,0,1,2)
 ```
 
-### General Workload Configuration
+#### list-append
 
-```
-workload.type= # workload type, currently only supports general, plan to add support for TPCC, etc.
-workload.history= # historical number of transactions
-workload.session= # number of simulated sessions
-workload.transaction= # number of transactions per session
-workload.operation= # number of operations per transaction
-workload.readproportion= # read operation proportion
-workload.key= # number of workload keys
-workload.distribution= # distribution type of transaction access keys, supports uniform, zipfan and hotspot
-```
+Refer to [jepsen history](https://github.com/jepsen-io/history).
 
-### Checker Configuration
+Example of history:
 
 ```
-checker.type= # consistency checking algorithm type, supports C4 and PolySI
-checker.isolation= # isolation level for the consistency checking algorithm, supports READ_COMMITTED, READ_ATOMICITY, CAUSAL_CONSISTENCY and SNAPSHOT_ISOLATION
+{:index 1, :type :invoke, :process 0, :value [ [ :append 1 1 ] [ :append 2 1 ] ]}
+{:index 2, :type :ok, :process 0, :value [ [ :append 1 1 ] [ :append 2 1 ] ]}
+{:index 3, :type :invoke, :process 1, :value [ [ :r 1 nil ] ]}
+{:index 4, :type :ok, :process 1, :value [ [ :r 1 [1] ] ]}
 ```
 
-### Performance Analysis Tool Configuration
+## How to use
 
-```
-profiler.enable= # whether to enable performance analysis, true/false
-```
+### Docker
 
-You can use `workload.variable` to specify a `workload` parameter and use `profiler` to perform performance analysis on `checker`, for example:
+Pull Docker image and deploy.
 
-```
-workload.history=3
-workload.session=[2,5,10,20,30]
-workload.variable=workload.session
-profiler.enable=true
+```bash
+docker pull ghcr.io/hengxin/IsoVista:main
+docker run --name IsoVista -p 8080:8080 -p 8000:8000 --rm -d ghcr.io/hengxin/IsoVista:main
 ```
 
-After running this configuration file, a `profiling_{timestamp}.csv` file will be obtained in the `result/` directory, which contains runtime data for the checking algorithm, such as:
+Then, use the browser to access the address http://127.0.0.1:8080 to use.
 
-| sessions | time (ms) | memory (MB) |
-| -------- | --------- | ----------- |
-| 2        | 7         | 34.2        |
-| 5        | 8         | 41.2        |
-| 10       | 11        | 52.2        |
-| 20       | 30        | 71.7        |
-| 30       | 38        | 93.2        |
+### Build on your own(not recommended)
 
-## Running Method
+Refer to the [Dockerfile](Dockerfile).
 
-After compilation, you can run DBTest with the following command:
+## How to extend IsoVista
 
-```
-java -jar ./target/DBTest-1.0-SNAPSHOT-shaded.jar config.properties
-```
+- [How to check a new database](docs/how-to-check-a-new-database.md)
+- [How to implement a new checker](docs/how-to-implement-a-new-checker.md)
 
-Since PolySI depends on monoSAT, you may see the following linking error when running PolySI:
+## Known limitations
 
-```
-Exception in thread "main" java.lang.UnsatisfiedLinkError: no monosat in java.library.path: /usr/java/packages/lib:/usr/lib64:/lib64:/lib:/usr/lib
-```
+- IsoVista utilizes multiple network connections to transmit data between the frontend and backend. In cases of network congestion, delays may occur, causing charts or tables to be displayed slowly or not promptly.
+- If the workload parameter is set very high (e.g., #session=10000), it might exhaust system resources. Therefore, IsoVista has imposed limits on the size of some parameters.
 
-You can add JVM parameter `-Djava.library.path=src/main/resource/libmonosat.so` or add `src/main/resource/libmonosat.so` to a directory in `java.library.path`. If the `libmonosat.so` provided in this repository cannot run on your environment, please compile it yourself using [monoSAT source code](https://github.com/sambayless/monosat).
+## Related GitHub Repository
 
-sudo docker run -p 8080:8080 -p 8000:8000 --rm -d ghcr.io/hengxin/db-testing-platform:dev-ui
+- [PolySI](https://github.com/amnore/PolySI)
+- [Viper](https://github.com/Khoury-srg/Viper)
+- [elle](https://github.com/jepsen-io/elle)
+- [elle-cli](https://github.com/ligurio/elle-cli)

docs/how-to-check-a-new-database.md

@@ -0,0 +1,60 @@
+# How to Check a New Database
+
+## JDBC Dependency
+Add the JDBC driver dependency for the new database to `pom.xml`.
+
+For example, the JDBC driver dependency for the MySQL is
+
+```
+<dependency>
+    <groupId>mysql</groupId>
+    <artifactId>mysql-connector-java</artifactId>
+    <version>8.0.33</version>
+</dependency>
+```
+
+## Collector
+
+Then, create a new package in the `src/main/java/collector` directory, and create two classes in this package to extend `Collector` and `DBClient`.
+
+Custom collector should have a String field `NAME` to represent the category of this database. 
+IsoVista uses this field in `config.properties` to select the database for the history collector.
+
+```java
+public static final String NAME = "MYSQL";
+```
+
+The collector needs to explicitly load the JDBC driver in the code to prevent conflicts between drivers.
+```java
+static {
+    try {
+        Class.forName("com.mysql.cj.jdbc.Driver");
+    } catch (ClassNotFoundException e) {
+        throw new RuntimeException(e);
+    }
+}
+```
+
+There are 4 methods the custom collector need to implement:
+
+- `collect`: Use `DBClient` and a thread pool to simulate multiple database client accesses to the database.
+- `crateTable`: Use JDBC to create a database table for subsequent history collection.
+- `createVariables`: Pre-insert the initial values of variables into the created database table.
+- `dropDatabase`: After completing the history collection, delete the database table.
+
+For details, please refer to `src/main/java/collector/mysql/MySQLClient.java`.
+
+## DBClient
+
+`DBClient` uses JDBC to connect to the database and converts a read-write(or list-append) operation into SQL and executes it.
+
+For example, the operation "write value 2 to variable 1" in SQL is
+```SQL
+UPDATE [table] SET val=2 WHERE var=1;
+```
+
+The operation "read value 4 from variable 3"
+
+```SQL
+SELECT val FROM dbtest.variables WHERE var=3;
+```

docs/how-to-implement-a-new-checker.md

@@ -0,0 +1,33 @@
+# How to Implement a New Checker
+
+Custom checkers should implement the `Checker` interface.
+You should add a static String field "NAME" in your custom checker class for IsoVista to identify it.
+
+The following methods should be implemented:
+
+## `verify`
+
+The detection code for the custom checker is implemented in this method. 
+If the given history does not have isolation violation, it returns true; otherwise, it returns false.
+
+
+If this custom checker is written in another language instead of Java, it can use JNI or start a subprocess to run the custom checker.
+If a subprocess is used to invoke the custom checker, after starting this subprocess, use `RuntimeInfoRecorder.addPid(process.pid());` so that IsoVista can monitor the CPU and memory usage of this subprocess.
+
+## `outputDotFile`
+
+After checking, if an isolation bug is discovered, you can use IsoVista to visualize this bug. 
+IsoVista accepts a DOT format string and includes built-in interpretation tools for SI and SER isolation bugs.
+
+For example:
+```java
+AnomalyInterpreter.interpretSI(history);
+```
+
+## `getProfileInfo`
+
+IsoVista performs a decomposition analysis that breaks down the checking time into stages.
+This method needs to return a `Map<String, Long>` to represent the duration (in milliseconds) of checking time at different stages by the custom checker, for display by IsoVista.
+For solver-based checkers, it can be divided into four stages: Construction, Encoding, Pruning, and Solving. For graph-based search checkers, it can be divided into two stages: Construction and Traversal.
+
+For details, please refer to `src/main/java/checker`.