diff --git a/Cargo.toml b/Cargo.toml index a2dfb3e3e..5178b9fb1 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -57,6 +57,13 @@ codegen-units = 1 panic = "abort" lto = true +[profile.antithesis] +inherits = "release" +debug = true +codegen-units = 1 +panic = "abort" +lto = true + [profile.bench-profile] inherits = "release" debug = true diff --git a/Dockerfile.antithesis b/Dockerfile.antithesis index 6305c12f0..7308ea97b 100644 --- a/Dockerfile.antithesis +++ b/Dockerfile.antithesis @@ -52,7 +52,7 @@ COPY --from=planner /app/vendored ./vendored/ RUN if [ "$antithesis" = "true" ]; then \ cp /opt/antithesis/libvoidstar.so /usr/lib/libvoidstar.so && \ export RUSTFLAGS="-Ccodegen-units=1 -Cpasses=sancov-module -Cllvm-args=-sanitizer-coverage-level=3 -Cllvm-args=-sanitizer-coverage-trace-pc-guard -Clink-args=-Wl,--build-id -L/usr/lib/ -lvoidstar" && \ - cargo build --bin limbo_stress --release; \ + cargo build --bin limbo_stress --antithesis; \ else \ cargo build --bin limbo_stress --release; \ fi @@ -62,14 +62,26 @@ RUN if [ "$antithesis" = "true" ]; then \ # FROM debian:bullseye-slim AS runtime -RUN apt-get update && apt-get install -y bash && rm -rf /var/lib/apt/lists/* +RUN apt-get update && apt-get install -y bash curl xz-utils python3 sqlite3 bc binutils pip && rm -rf /var/lib/apt/lists/* +RUN curl --proto '=https' --tlsv1.2 -LsSf \ + https://github.com/tursodatabase/limbo/releases/latest/download/limbo_cli-installer.sh | sh +RUN bash -c "source $HOME/.limbo/env" +RUN pip install antithesis pylimbo --break-system-packages WORKDIR /app EXPOSE 8080 COPY --from=builder /usr/lib/libvoidstar.so* /usr/lib/ COPY --from=builder /app/target/release/limbo_stress /bin/limbo_stress +COPY --from=builder /app/target/antithesis/limbo_stress /symbols COPY stress/docker-entrypoint.sh /bin RUN chmod +x /bin/docker-entrypoint.sh -ENTRYPOINT ["/bin/docker-entrypoint.sh"] -ENV RUST_BACKTRACE=1 -CMD ["/bin/limbo_stress"] + +COPY ./antithesis-tests/bank-test/*.py /opt/antithesis/test/v1/bank-test/ +COPY ./antithesis-tests/stress-composer/*.py /opt/antithesis/test/v1/stress-composer/ +COPY ./antithesis-tests/stress /opt/antithesis/test/v1/stress +RUN chmod 777 -R /opt/antithesis/test/v1 + +RUN mkdir /opt/antithesis/catalog +RUN ln -s /opt/antithesis/test/v1/bank-test/*.py /opt/antithesis/catalog + +ENTRYPOINT ["/bin/docker-entrypoint.sh"] \ No newline at end of file diff --git a/antithesis-tests/bank-test/anytime_validate.py b/antithesis-tests/bank-test/anytime_validate.py new file mode 100755 index 000000000..8bfb11304 --- /dev/null +++ b/antithesis-tests/bank-test/anytime_validate.py @@ -0,0 +1,26 @@ +#!/usr/bin/env -S python3 -u + +import limbo +from antithesis.random import get_random +from antithesis.assertions import always + +con = limbo.connect("bank_test.db") +cur = con.cursor() + +initial_state = cur.execute(f''' + SELECT * FROM initial_state +''').fetchone() + +curr_total = cur.execute(f''' + SELECT SUM(balance) AS total FROM accounts; +''').fetchone() + +always( + initial_state[1] == curr_total[0], + '[Anytime] Initial balance always equals current balance', + { + 'init_bal': initial_state[1], + 'curr_bal': curr_total[0] + } +) + diff --git a/antithesis-tests/bank-test/eventually_validate.py b/antithesis-tests/bank-test/eventually_validate.py new file mode 100755 index 000000000..413d04aae --- /dev/null +++ b/antithesis-tests/bank-test/eventually_validate.py @@ -0,0 +1,26 @@ +#!/usr/bin/env -S python3 -u + +import limbo +from antithesis.random import get_random +from antithesis.assertions import always + +con = limbo.connect("bank_test.db") +cur = con.cursor() + +initial_state = cur.execute(f''' + SELECT * FROM initial_state +''').fetchone() + +curr_total = cur.execute(f''' + SELECT SUM(balance) AS total FROM accounts; +''').fetchone() + +always( + initial_state[1] == curr_total[0], + '[Eventually] Initial balance always equals current balance', + { + 'init_bal': initial_state[1], + 'curr_bal': curr_total[0] + } +) + diff --git a/antithesis-tests/bank-test/finally_validate.py b/antithesis-tests/bank-test/finally_validate.py new file mode 100755 index 000000000..fa90b15f8 --- /dev/null +++ b/antithesis-tests/bank-test/finally_validate.py @@ -0,0 +1,26 @@ +#!/usr/bin/env -S python3 -u + +import limbo +from antithesis.random import get_random +from antithesis.assertions import always + +con = limbo.connect("bank_test.db") +cur = con.cursor() + +initial_state = cur.execute(f''' + SELECT * FROM initial_state +''').fetchone() + +curr_total = cur.execute(f''' + SELECT SUM(balance) AS total FROM accounts; +''').fetchone() + +always( + initial_state[1] == curr_total[0], + '[Finally] Initial balance always equals current balance', + { + 'init_bal': initial_state[1], + 'curr_bal': curr_total[0] + } +) + diff --git a/antithesis-tests/bank-test/first_setup.py b/antithesis-tests/bank-test/first_setup.py new file mode 100755 index 000000000..df833b96e --- /dev/null +++ b/antithesis-tests/bank-test/first_setup.py @@ -0,0 +1,47 @@ +#!/usr/bin/env -S python3 -u + +import limbo +from antithesis.random import get_random + +con = limbo.connect("bank_test.db") +cur = con.cursor() + +# drop accounts table if it exists and create a new table +cur.execute(f''' + DROP TABLE IF EXISTS accounts; +''') + +cur.execute(f''' + CREATE TABLE accounts ( + account_id INTEGER PRIMARY KEY AUTOINCREMENT, + balance REAL NOT NULL DEFAULT 0.0 + ); +''') + +# randomly create up to 100 accounts with a balance up to 1e9 +total = 0 +num_accts = get_random() % 100 +for i in range(num_accts): + bal = get_random() % 1e9 + total += bal + cur.execute(f''' + INSERT INTO accounts (balance) + VALUES ({bal}) + ''') + +# drop initial_state table if it exists and create a new table +cur.execute(f''' + DROP TABLE IF EXISTS initial_state; +''') +cur.execute(f''' + CREATE TABLE initial_state ( + num_accts INTEGER, + total REAL + ); +''') + +# store initial state in the table +cur.execute(f''' + INSERT INTO initial_state (num_accts, total) + VALUES ({num_accts}, {total}) +''') \ No newline at end of file diff --git a/antithesis-tests/bank-test/parallel_driver_generate_transaction.py b/antithesis-tests/bank-test/parallel_driver_generate_transaction.py new file mode 100755 index 000000000..9e96260ba --- /dev/null +++ b/antithesis-tests/bank-test/parallel_driver_generate_transaction.py @@ -0,0 +1,54 @@ +#!/usr/bin/env -S python3 -u + +import limbo +import logging +from logging.handlers import RotatingFileHandler +from antithesis.random import get_random + +handler = RotatingFileHandler(filename='bank_test.log', mode='a', maxBytes=1*1024*1024, backupCount=5, encoding=None, delay=0) +handler.setLevel(logging.INFO) + +logger = logging.getLogger('root') +logger.setLevel(logging.INFO) + +logger.addHandler(handler) + +con = limbo.connect("bank_test.db") +cur = con.cursor() + +length = cur.execute("SELECT num_accts FROM initial_state").fetchone()[0] + +def transaction(): + # check that sender and recipient are different + sender = get_random() % length + 1 + recipient = get_random() % length + 1 + if sender != recipient: + # get a random value to transfer between accounts + value = get_random() % 1e9 + + logger.info(f"Sender ID: {sender} | Recipient ID: {recipient} | Txn Val: {value}") + + cur.execute("BEGIN TRANSACTION;") + + # subtract value from balance of the sender account + cur.execute(f''' + UPDATE accounts + SET balance = balance - {value} + WHERE account_id = {sender}; + ''') + + # add value to balance of the recipient account + cur.execute(f''' + UPDATE accounts + SET balance = balance + {value} + WHERE account_id = {recipient}; + ''') + + cur.execute("COMMIT;") + +# run up to 100 transactions +iterations = get_random() % 100 +# logger.info(f"Starting {iterations} iterations") +for i in range(iterations): + transaction() +# logger.info(f"Finished {iterations} iterations") diff --git a/antithesis-tests/stress-composer/first_setup.py b/antithesis-tests/stress-composer/first_setup.py new file mode 100755 index 000000000..cccf5e015 --- /dev/null +++ b/antithesis-tests/stress-composer/first_setup.py @@ -0,0 +1,75 @@ +#!/usr/bin/env -S python3 -u + +import json +import glob +import os +import limbo +from antithesis.random import get_random, random_choice + +constraints = ['NOT NULL', 'UNIQUE', ''] +data_type = ['INTEGER', 'REAL', 'TEXT', 'BLOB', 'NUMERIC'] + +# remove any existing db files +for f in glob.glob('*.db'): + try: + os.remove(f) + except OSError: + pass + +for f in glob.glob('*.db-wal'): + try: + os.remove(f) + except OSError: + pass + +# store initial states in a separate db +con_init = limbo.connect('init_state.db') +cur_init = con_init.cursor() +cur_init.execute('CREATE TABLE schemas (schema TEXT, tbl INT PRIMARY KEY)') +cur_init.execute('CREATE TABLE tables (count INT)') + +con = limbo.connect('stress_composer.db') +cur = con.cursor() + +tbl_count = max(1, get_random() % 10) + +cur_init.execute(f'INSERT INTO tables (count) VALUES ({tbl_count})') + +schemas = [] +for i in range(tbl_count): + col_count = max(1, get_random() % 10) + pk = get_random() % col_count + + schema = { + 'table': i, + 'colCount': col_count, + 'pk': pk + } + + cols = [] + cols_str = '' + for j in range(col_count): + col_data_type = random_choice(data_type) + col_constraint_1 = random_choice(constraints) + col_constraint_2 = random_choice(constraints) + + col = f'col_{j} {col_data_type} {col_constraint_1} {col_constraint_2 if col_constraint_2 != col_constraint_1 else ""}' if j != pk else f'col_{j} {col_data_type} PRIMARY KEY NOT NULL' + + cols.append(col) + + schema[f'col_{j}'] = { + 'data_type': col_data_type, + 'constraint1': col_constraint_1 if j != pk else 'PRIMARY KEY', + 'constraint2': col_constraint_2 if col_constraint_1 != col_constraint_2 else "" if j != pk else 'NOT NULL', + } + + cols_str = ', '.join(cols) + + schemas.append(schema) + cur_init.execute(f"INSERT INTO schemas (schema, tbl) VALUES ('{json.dumps(schema)}', {i})") + + cur.execute(f''' + CREATE TABLE tbl_{i} ({cols_str}) + ''') + +print(f'DB Schemas\n------------\n{json.dumps(schemas, indent=2)}') \ No newline at end of file diff --git a/antithesis-tests/stress-composer/parallel_driver_delete.py b/antithesis-tests/stress-composer/parallel_driver_delete.py new file mode 100755 index 000000000..6d0331f56 --- /dev/null +++ b/antithesis-tests/stress-composer/parallel_driver_delete.py @@ -0,0 +1,33 @@ +#!/usr/bin/env -S python3 -u + +import json +import limbo +from utils import generate_random_value +from antithesis.random import get_random + +# Get initial state +con_init = limbo.connect('init_state.db') +cur_init = con_init.cursor() + +tbl_len = cur_init.execute('SELECT count FROM tables').fetchone()[0] +selected_tbl = get_random() % tbl_len +tbl_schema = json.loads(cur_init.execute(f'SELECT schema FROM schemas WHERE tbl = {selected_tbl}').fetchone()[0]) + +# get primary key column +pk = tbl_schema['pk'] +# get non-pk columns +cols = [f'col_{col}' for col in range(tbl_schema['colCount']) if col != pk] + +con = limbo.connect('stress_composer.db') +cur = con.cursor() + +deletions = get_random() % 100 +print(f'Attempt to delete {deletions} rows in tbl_{selected_tbl}...') + +for i in range(deletions): + where_clause = f"col_{pk} = {generate_random_value(tbl_schema[f'col_{pk}']['data_type'])}" + + cur.execute(f''' + DELETE FROM tbl_{selected_tbl} WHERE {where_clause} + ''') + diff --git a/antithesis-tests/stress-composer/parallel_driver_insert.py b/antithesis-tests/stress-composer/parallel_driver_insert.py new file mode 100755 index 000000000..89d4daea0 --- /dev/null +++ b/antithesis-tests/stress-composer/parallel_driver_insert.py @@ -0,0 +1,31 @@ +#!/usr/bin/env -S python3 -u + +import json +import limbo +from utils import generate_random_value +from antithesis.random import get_random + + +# Get initial state +con_init = limbo.connect('init_state.db') +cur_init = con_init.cursor() + +tbl_len = cur_init.execute('SELECT count FROM tables').fetchone()[0] +selected_tbl = get_random() % tbl_len +tbl_schema = json.loads(cur_init.execute(f'SELECT schema FROM schemas WHERE tbl = {selected_tbl}').fetchone()[0]) +cols = ', '.join([f'col_{col}' for col in range(tbl_schema['colCount'])]) + +con = limbo.connect('stress_composer.db') +cur = con.cursor() + +# insert up to 100 rows in the selected table +insertions = get_random() % 100 +print(f'Inserting {insertions} rows...') + +for i in range(insertions): + values = [generate_random_value(tbl_schema[f'col_{col}']['data_type']) for col in range(tbl_schema['colCount'])] + cur.execute(f''' + INSERT INTO tbl_{selected_tbl} ({cols}) + VALUES ({', '.join(values)}) + ''') + diff --git a/antithesis-tests/stress-composer/parallel_driver_update.py b/antithesis-tests/stress-composer/parallel_driver_update.py new file mode 100755 index 000000000..fc707cb8b --- /dev/null +++ b/antithesis-tests/stress-composer/parallel_driver_update.py @@ -0,0 +1,45 @@ +#!/usr/bin/env -S python3 -u + +import json +import limbo +from utils import generate_random_value +from antithesis.random import get_random + +# Get initial state +con_init = limbo.connect('init_state.db') +cur_init = con_init.cursor() + +tbl_len = cur_init.execute('SELECT count FROM tables').fetchone()[0] +selected_tbl = get_random() % tbl_len +tbl_schema = json.loads(cur_init.execute(f'SELECT schema FROM schemas WHERE tbl = {selected_tbl}').fetchone()[0]) + +# get primary key column +pk = tbl_schema['pk'] +# get non-pk columns +cols = [f'col_{col}' for col in range(tbl_schema['colCount']) if col != pk] +# print(cols) +con = limbo.connect('stress_composer.db') +cur = con.cursor() + +# insert up to 100 rows in the selected table +updates = get_random() % 100 +print(f'Attempt to update {updates} rows in tbl_{selected_tbl}...') + +for i in range(updates): + set_clause = '' + if tbl_schema['colCount'] == 1: + set_clause = f"col_{pk} = {generate_random_value(tbl_schema[f'col_{pk}']['data_type'])}" + else: + values = [] + for col in cols: + # print(col) + values.append(f"{col} = {generate_random_value(tbl_schema[col]['data_type'])}") + set_clause = ', '.join(values) + + where_clause = f"col_{pk} = {generate_random_value(tbl_schema[f'col_{pk}']['data_type'])}" + # print(where_clause) + + cur.execute(f''' + UPDATE tbl_{selected_tbl} SET {set_clause} WHERE {where_clause} + ''') + diff --git a/antithesis-tests/stress-composer/utils.py b/antithesis-tests/stress-composer/utils.py new file mode 100755 index 000000000..f99052bf3 --- /dev/null +++ b/antithesis-tests/stress-composer/utils.py @@ -0,0 +1,20 @@ +import string +from antithesis.random import get_random, random_choice + +def generate_random_identifier(type: str, num: int): + return ''.join(type, '_', get_random() % num) + +def generate_random_value(type: str): + match type: + case 'INTEGER': + return str(get_random() % 100) + case 'REAL': + return '{:.2f}'.format(get_random() % 100 / 100.0) + case 'TEXT': + return f"'{''.join(random_choice(string.ascii_lowercase) for _ in range(5))}'" + case 'BLOB': + return f"x'{''.join(random_choice(string.ascii_lowercase) for _ in range(5)).encode().hex()}'" + case 'NUMERIC': + return str(get_random() % 100) + case _: + return NULL \ No newline at end of file diff --git a/antithesis-tests/stress/singleton_driver_stress.sh b/antithesis-tests/stress/singleton_driver_stress.sh new file mode 100755 index 000000000..06f27223f --- /dev/null +++ b/antithesis-tests/stress/singleton_driver_stress.sh @@ -0,0 +1,3 @@ +#!/usr/bin/env bash + +/bin/limbo_stress \ No newline at end of file diff --git a/stress/docker-compose.yaml b/stress/docker-compose.yaml index 13b1149a8..c6e081aac 100644 --- a/stress/docker-compose.yaml +++ b/stress/docker-compose.yaml @@ -1,4 +1,7 @@ services: - workload: - image: us-central1-docker.pkg.dev/molten-verve-216720/turso-repository/limbo-workload:antithesis-latest - command: [ "/bin/limbo_stress" ] + limbo: + container_name: limbo + hostname: limbo + image: limbo:latest + entrypoint: ["/bin/docker-entrypoint.sh"] + command: ["sleep", "infinity"] \ No newline at end of file diff --git a/stress/docker-entrypoint.sh b/stress/docker-entrypoint.sh index a09822694..1aa226912 100644 --- a/stress/docker-entrypoint.sh +++ b/stress/docker-entrypoint.sh @@ -1,5 +1,7 @@ #!/bin/bash +echo '{"antithesis_setup": { "status": "complete", "details": null }}' > $ANTITHESIS_OUTPUT_DIR/sdk.jsonl + set -Eeuo pipefail exec "$@" diff --git a/stress/main.rs b/stress/main.rs index e8b61b459..a00b9fb66 100644 --- a/stress/main.rs +++ b/stress/main.rs @@ -321,7 +321,7 @@ fn generate_plan(opts: &Opts) -> Result Result<(), Box> { "num_nodes": num_nodes, "main_node_id": main_id, }); - lifecycle::setup_complete(&startup_data); + // lifecycle::setup_complete(&startup_data); antithesis_init(); let mut opts = Opts::parse();