Merge 'Add Antithesis Tests' from eric-dinh-antithesis

This PR adds 2 autonomous test suites for use with Antithesis: `bank-
test` and `stress-composer`. It also modifies the existing
`limbo_stress` test to run as a singleton and modifies other Antithesis-
related configuration files.
**bank-test**
- `first_setup.py`
  - initializes a DB table with columns accounts and balance
  - generates random balances for each account
  - stores initial state of the table
- `parallel_driver_generate_transaction.py`
  - selects 2 accounts from the table as sender and receiver
  - generates a random value which is subtracted from sender and added
to receiver
- `anytime/eventually/finally_validate.py`
  - checks that sum of initial balances == sum of current balances
**stress-composer**
- Breaks `limbo_stress` into component parts
- `first_setup.py`
  - creates up to 10 tables with up to 10 columns
  - stores table details in a separate db
- `parallel_driver_insert.py`
  - randomly generates and executes up to 100 insert statements into a
single table using random values derived from the table details
- `parallel_driver_update.py`
  - randomly generates and executes up to 100 updates into a single
table using random values derived from the table details
- `parallel_driver_delete.py`
  - randomly generates and executes up to 100 deletes from a single
table using random values derived from the table details

Closes #1401

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

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"]

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]
+    }
+)
+

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]
+    }
+)
+

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]
+    }
+)
+

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})
+''')

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")

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)}')

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}
+    ''')
+

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)})
+    ''')
+

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}
+    ''')
+

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

antithesis-tests/stress/singleton_driver_stress.sh

@@ -0,0 +1,3 @@
+#!/usr/bin/env bash
+
+/bin/limbo_stress

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"]

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 "$@"

stress/main.rs

@@ -321,7 +321,7 @@ fn generate_plan(opts: &Opts) -> Result<Plan, Box<dyn std::error::Error + Send +
         let mut queries = vec![];
         for _ in 0..opts.nr_iterations {
             let sql = generate_random_statement(&schema);
-            writeln!(log_file, "{}", sql)?;
+            // writeln!(log_file, "{}", sql)?;
             queries.push(sql);
         }
         plan.queries_per_thread.push(queries);
@@ -396,7 +396,7 @@ async fn main() -> Result<(), Box<dyn std::error::Error + Send + Sync>> {
         "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();