diff --git a/benchmarks/specfs_bench/README.md b/benchmarks/specfs_bench/README.md
new file mode 100644
index 00000000..fe44a4e8
--- /dev/null
+++ b/benchmarks/specfs_bench/README.md
@@ -0,0 +1,121 @@
+# SpecFS Benchmark
+
+## Scenario Description
+
+Formal specifications are a cornerstone of building trustworthy systems software — particularly file systems, where subtle correctness bugs can cause data loss or security breaches. SpecFS Bench evaluates whether LLMs can translate structured, Hoare-logic-style specifications of file system modules into correct, modular C implementations that match expert-written ground truth.
+
+### Task Details
+
+- **Input**
+  - Specification files (`.spec`) from `data/spec/`
+  - Generation / Judge prompt template
+  - Generation / Judge Model
+- **Output**
+  - Generated C source file per spec under `outputs/<run>/generated/<relative_path>.c`
+  - Per-case generation records (`generation_results.jsonl`)
+  - Per-case judge verdicts (`judge_results.jsonl`)
+  - Aggregated summary (`summary.json`)
+- **Evaluation**
+  - `LLM-as-a-judge`: compares generated code against ground-truth C code under the same spec, scoring functional equivalence on a 0–10 scale with verdict (`pass` / `partial` / `fail`), a short rationale, and a list of differences.
+
+### Key Features
+
+- Structured spec format combining natural-language intent with formal pre/post-conditions
+- Modular generation: the model produces a single module while reusing pre-defined APIs from other modules listed in `[RELY]`
+- Fully automated two-phase pipeline: code generation → LLM-based judging
+- Configurable generation and judge models
+
+## Benchmark Setup
+
+### Prerequisites
+
+- Python 3.9+
+- LLM endpoint configured in `env.toml`
+
+### Configuration
+
+Copy the example config and fill in credentials:
+
+```bash
+cp env.toml.example env.toml
+```
+
+Edit `benchmarks/specfs/env.toml`:
+
+```toml
+[llm]
+OPENAI_API_KEY = "your_key_here"
+OPENAI_API_BASE = "your_url_here"
+```
+
+If no local `env.toml` is found, the benchmark falls back to the workspace-level `env.toml` one directory above, and finally to environment variables.
+
+### Install Dependencies
+
+```bash
+cd benchmarks/specfs
+./install.sh
+```
+
+This script creates `.venv/` and installs `benchmarks/specfs/requirements.txt`.
+
+### Run the Benchmark
+
+```bash
+./run.sh <model_name>
+```
+
+The wrapper invokes `src/main.py`, which:
+
+1. Discovers all `.spec` files under `data/spec/` recursively.
+2. Generates a C implementation for each spec using the generation prompt.
+3. Judges each generated file against the corresponding ground truth under `data/code/` using the judge prompt.
+4. Writes results under:
+
+```
+outputs/specfsbench__<model>__judge_<judge_model>__<timestamp>/
+├── generated/              # Generated C files mirroring data/spec/ layout
+├── generation_results.jsonl
+├── judge_results.jsonl
+└── summary.json            # Aggregated stats and average score
+```
+
+## Evaluation Metrics
+
+SpecFS Bench uses an LLM-as-a-judge protocol to score each generated module against the reference implementation under the same spec.
+
+For every case, the judge receives the spec, the generated code, and the ground-truth code, and returns a structured JSON verdict:
+
+```json
+{
+  "score": 0-10,
+  "verdict": "pass" | "partial" | "fail",
+  "summary": "short rationale",
+  "differences": ["difference 1", "difference 2"]
+}
+```
+
+Aggregated metrics can be found in `summary.json`.
+
+
+## Project Structure
+
+```
+benchmarks/specfs/
+├── data/
+│   ├── spec/                    # Spec files (.spec) organized by category
+│   └── code/                    # Ground-truth C implementations (mirrors data/spec/)
+├── src/
+│   ├── main.py                  # Entry point: discover → generate → judge → summarize
+│   ├── evaluator.py             # LLM-as-a-judge evaluator
+│   ├── genspec_prompt.md        # Prompt template for code generation
+│   └── judge_prompt.md          # Prompt template for the LLM judge
+├── tests/
+├── logs/                        # Run and install logs
+├── outputs/                     # Per-run outputs (generated code, jsonl, summary)
+├── env.toml.example             # Example configuration
+├── install.sh                   # Environment setup script
+├── run.sh                       # Benchmark entry wrapper
+├── requirements.txt
+└── README.md
+```
diff --git a/benchmarks/specfs_bench/data/code/file/file_allocate.c b/benchmarks/specfs_bench/data/code/file/file_allocate.c
new file mode 100644
index 00000000..96037582
--- /dev/null
+++ b/benchmarks/specfs_bench/data/code/file/file_allocate.c
@@ -0,0 +1,21 @@
+#include "file.h"
+
+void file_allocate(struct inode *node, unsigned offset, unsigned len) {
+    unsigned start_page = offset / PG_SIZE;
+    unsigned end_page = (offset + len - 1) / PG_SIZE;
+
+    if (end_page >= INDEXTB_NUM) {
+        end_page = INDEXTB_NUM - 1;
+    }
+
+    for (unsigned i = start_page; i <= end_page; i++) {
+        if (node->file->index[i] == NULL) {
+            node->file->index[i] = malloc_page();
+        }
+    }
+
+    unsigned new_size = offset + len;
+    if (new_size > node->size) {
+        node->size = new_size;
+    }
+}
\ No newline at end of file
diff --git a/benchmarks/specfs_bench/data/code/file/file_clear.c b/benchmarks/specfs_bench/data/code/file/file_clear.c
new file mode 100644
index 00000000..7cd52e7d
--- /dev/null
+++ b/benchmarks/specfs_bench/data/code/file/file_clear.c
@@ -0,0 +1,7 @@
+#include "file.h"
+
+void file_clear(struct inode *node, unsigned start, unsigned len) {
+    // According to [RELY], file_write writes zeroes if data is NULL.
+    // We utilize this behavior to clear the specified range.
+    file_write(node, start, len, NULL);
+}
\ No newline at end of file
diff --git a/benchmarks/specfs_bench/data/code/file/file_read.c b/benchmarks/specfs_bench/data/code/file/file_read.c
new file mode 100644
index 00000000..32ade887
--- /dev/null
+++ b/benchmarks/specfs_bench/data/code/file/file_read.c
@@ -0,0 +1,22 @@
+#include "file.h"
+
+void file_read(struct inode *node, unsigned offset, unsigned len, char *data) {
+    unsigned current_offset = offset;
+    unsigned remaining = len;
+    char *dst = data;
+
+    while (remaining > 0) {
+        unsigned page_idx = current_offset >> 12;
+        unsigned page_offset = current_offset & 0xFFF;
+        unsigned char *page_ptr = node->file->index[page_idx];
+
+        unsigned bytes_in_page = PG_SIZE - page_offset;
+        unsigned to_copy = (remaining < bytes_in_page) ? remaining : bytes_in_page;
+
+        memcpy(dst, page_ptr + page_offset, to_copy);
+
+        dst += to_copy;
+        current_offset += to_copy;
+        remaining -= to_copy;
+    }
+}
\ No newline at end of file
diff --git a/benchmarks/specfs_bench/data/code/file/file_write.c b/benchmarks/specfs_bench/data/code/file/file_write.c
new file mode 100644
index 00000000..5ee289f1
--- /dev/null
+++ b/benchmarks/specfs_bench/data/code/file/file_write.c
@@ -0,0 +1,35 @@
+#include "file.h"
+
+void file_write(struct inode *node, unsigned offset, unsigned len, const char *data) {
+    if (len == 0 || node == NULL || node->file == NULL) {
+        return;
+    }
+
+    struct indextb *tb = node->file;
+    unsigned current_offset = offset;
+    unsigned remaining = len;
+    unsigned data_idx = 0;
+
+    while (remaining > 0) {
+        unsigned page_idx = current_offset / PAGE_SIZE;
+        unsigned page_offset = current_offset % PAGE_SIZE;
+        unsigned bytes_in_page = PAGE_SIZE - page_offset;
+        unsigned bytes_to_write = (remaining < bytes_in_page) ? remaining : bytes_in_page;
+
+        unsigned char *page = tb->index[page_idx];
+
+        if (data != NULL) {
+            for (unsigned i = 0; i < bytes_to_write; i++) {
+                page[page_offset + i] = data[data_idx + i];
+            }
+        } else {
+            for (unsigned i = 0; i < bytes_to_write; i++) {
+                page[page_offset + i] = 0;
+            }
+        }
+
+        current_offset += bytes_to_write;
+        remaining -= bytes_to_write;
+        data_idx += bytes_to_write;
+    }
+}
\ No newline at end of file
diff --git a/benchmarks/specfs_bench/data/code/inode/inode_delete.c b/benchmarks/specfs_bench/data/code/inode/inode_delete.c
new file mode 100644
index 00000000..0e9c6c6e
--- /dev/null
+++ b/benchmarks/specfs_bench/data/code/inode/inode_delete.c
@@ -0,0 +1,28 @@
+#include "inode.h"
+
+struct inode* inode_delete(struct inode* inum, char* name) {
+    unsigned int n = hash_name(name);
+    struct entry *prev = NULL;
+    struct entry *curr = inum->dir->tb[n];
+    
+    while (curr != NULL) {
+        if (strcmp(curr->name, name) == 0) {
+            struct inode* ret_inum = curr->inum;
+            
+            if (prev == NULL) {
+                inum->dir->tb[n] = curr->next;
+            } else {
+                prev->next = curr->next;
+            }
+            
+            free_entry(curr);
+            inum->size--;
+            
+            return ret_inum;
+        }
+        prev = curr;
+        curr = curr->next;
+    }
+    
+    return NULL;
+}
\ No newline at end of file
diff --git a/benchmarks/specfs_bench/data/code/inode/inode_find.c b/benchmarks/specfs_bench/data/code/inode/inode_find.c
new file mode 100644
index 00000000..517f2b3e
--- /dev/null
+++ b/benchmarks/specfs_bench/data/code/inode/inode_find.c
@@ -0,0 +1,15 @@
+#include "inode.h"
+
+struct inode *inode_find(struct inode *node, char *name) {
+    unsigned int n = hash_name(name);
+    struct entry *curr = node->dir->tb[n];
+
+    while (curr != NULL) {
+        if (strcmp(curr->name, name) == 0) {
+            return (struct inode *)curr->inum;
+        }
+        curr = curr->next;
+    }
+
+    return NULL;
+}
\ No newline at end of file
diff --git a/benchmarks/specfs_bench/data/code/inode/inode_insert.c b/benchmarks/specfs_bench/data/code/inode/inode_insert.c
new file mode 100644
index 00000000..1b4a32d9
--- /dev/null
+++ b/benchmarks/specfs_bench/data/code/inode/inode_insert.c
@@ -0,0 +1,25 @@
+#include "inode.h"
+
+int inode_insert(struct inode* cur, struct inode* inum, char* name) {
+    unsigned int n = hash_name(name);
+    struct entry *new_entry = malloc_entry();
+
+    if (new_entry == NULL) {
+        return 1;
+    }
+
+    char *new_name = malloc_string(name);
+    if (new_name == NULL) {
+        free(new_entry);
+        return 1;
+    }
+
+    new_entry->name = new_name;
+    new_entry->inum = inum;
+    new_entry->next = cur->dir->tb[n];
+
+    cur->dir->tb[n] = new_entry;
+    cur->size++;
+
+    return 0;
+}
\ No newline at end of file
diff --git a/benchmarks/specfs_bench/data/code/inode/inode_read.c b/benchmarks/specfs_bench/data/code/inode/inode_read.c
new file mode 100644
index 00000000..3c83f445
--- /dev/null
+++ b/benchmarks/specfs_bench/data/code/inode/inode_read.c
@@ -0,0 +1,22 @@
+#include "inode.h"
+
+struct read_ret* inode_read(struct inode* node, unsigned len, unsigned offset) {
+    struct read_ret* ret = malloc_readret();
+
+    if (offset >= node->size || len == 0) {
+        ret->num = 0;
+        ret->buf = NULL;
+        return ret;
+    }
+
+    unsigned remaining = node->size - offset;
+    unsigned actual_len = (len < remaining) ? len : remaining;
+
+    char* buf = malloc_buffer(actual_len);
+    file_read(node, offset, actual_len, buf);
+
+    ret->buf = buf;
+    ret->num = actual_len;
+
+    return ret;
+}
\ No newline at end of file
diff --git a/benchmarks/specfs_bench/data/code/inode/inode_truncate.c b/benchmarks/specfs_bench/data/code/inode/inode_truncate.c
new file mode 100644
index 00000000..563b09e8
--- /dev/null
+++ b/benchmarks/specfs_bench/data/code/inode/inode_truncate.c
@@ -0,0 +1,13 @@
+#include "inode.h"
+
+void inode_truncate(struct inode* node, unsigned size) {
+    if (size < node->size) {
+        file_clear(node, size, node->size - size);
+        node->size = size;
+    } else if (size > node->size) {
+        unsigned diff = size - node->size;
+        file_allocate(node, node->size, diff);
+        file_clear(node, node->size, diff);
+        node->size = size;
+    }
+}
\ No newline at end of file
diff --git a/benchmarks/specfs_bench/data/code/inode/inode_write.c b/benchmarks/specfs_bench/data/code/inode/inode_write.c
new file mode 100644
index 00000000..a61b7ed2
--- /dev/null
+++ b/benchmarks/specfs_bench/data/code/inode/inode_write.c
@@ -0,0 +1,34 @@
+#include "inode.h"
+
+unsigned inode_write(struct inode* node, const char* buffer, unsigned len, unsigned offset) {
+    unsigned end = offset + len;
+
+    // Calculate the new size, capped at MAX_FILE_SIZE
+    if (end > MAX_FILE_SIZE) {
+        end = MAX_FILE_SIZE;
+    }
+
+    // If the offset is beyond the calculated end, no bytes can be written
+    if (offset >= end) {
+        return 0;
+    }
+
+    unsigned new_size = end;
+    unsigned written = new_size - offset;
+
+    // If the write extends beyond the current file size, allocate and clear new space
+    if (new_size > node->size) {
+        unsigned alloc_start = node->size;
+        unsigned alloc_len = new_size - node->size;
+
+        file_allocate(node, alloc_start, alloc_len);
+        file_clear(node, alloc_start, alloc_len);
+
+        node->size = new_size;
+    }
+
+    // Write the data to the file
+    file_write(node, offset, written, buffer);
+
+    return written;
+}
\ No newline at end of file
diff --git a/benchmarks/specfs_bench/data/code/interface-util/check_del.c b/benchmarks/specfs_bench/data/code/interface-util/check_del.c
new file mode 100644
index 00000000..20538e86
--- /dev/null
+++ b/benchmarks/specfs_bench/data/code/interface-util/check_del.c
@@ -0,0 +1,29 @@
+#include "interface-util.h"
+
+int check_del(struct inode *cur, char *name) {
+    struct inode *target;
+
+    // Pre-condition: cur lock is already held
+
+    if (cur == NULL) {
+        return 1;
+    }
+
+    target = inode_find(cur, name);
+
+    if (target == NULL) {
+        unlock(cur);
+        return 1;
+    }
+
+    // Check if deletion is permissible (file or empty directory)
+    if (target->mode != DIR_MODE || target->size == 0) {
+        // Success: lock target, return with both locks held
+        lock(target);
+        return 0;
+    } else {
+        // Failure: non-empty directory, release cur lock
+        unlock(cur);
+        return 1;
+    }
+}
\ No newline at end of file
diff --git a/benchmarks/specfs_bench/data/code/interface-util/check_dir.c b/benchmarks/specfs_bench/data/code/interface-util/check_dir.c
new file mode 100644
index 00000000..804f3762
--- /dev/null
+++ b/benchmarks/specfs_bench/data/code/interface-util/check_dir.c
@@ -0,0 +1,11 @@
+#include "interface-util.h"
+
+int check_dir(struct inode *inum) {
+    if (inum == NULL || inum->mode != DIR_MODE) {
+        if (inum != NULL) {
+            unlock(inum);
+        }
+        return 1;
+    }
+    return 0;
+}
\ No newline at end of file
diff --git a/benchmarks/specfs_bench/data/code/interface-util/check_file.c b/benchmarks/specfs_bench/data/code/interface-util/check_file.c
new file mode 100644
index 00000000..a113a812
--- /dev/null
+++ b/benchmarks/specfs_bench/data/code/interface-util/check_file.c
@@ -0,0 +1,14 @@
+#include "interface-util.h"
+
+int check_file(struct inode *inum) {
+    if (inum == NULL) {
+        return 1;
+    }
+
+    if (inum->mode == DIR_MODE) {
+        unlock(inum);
+        return 1;
+    }
+
+    return 0;
+}
\ No newline at end of file
diff --git a/benchmarks/specfs_bench/data/code/interface-util/check_ins.c b/benchmarks/specfs_bench/data/code/interface-util/check_ins.c
new file mode 100644
index 00000000..3a9d60df
--- /dev/null
+++ b/benchmarks/specfs_bench/data/code/interface-util/check_ins.c
@@ -0,0 +1,24 @@
+#include "interface-util.h"
+
+int check_ins(struct inode *cur, char *name) {
+    if (cur == NULL) {
+        return 1;
+    }
+
+    if (cur->mode != DIR_MODE) {
+        unlock(cur);
+        return 1;
+    }
+
+    if (cur->size >= MAX_DIR_SIZE) {
+        unlock(cur);
+        return 1;
+    }
+
+    if (inode_find(cur, name) != NULL) {
+        unlock(cur);
+        return 1;
+    }
+
+    return 0;
+}
\ No newline at end of file
diff --git a/benchmarks/specfs_bench/data/code/interface-util/check_open.c b/benchmarks/specfs_bench/data/code/interface-util/check_open.c
new file mode 100644
index 00000000..5fa90f60
--- /dev/null
+++ b/benchmarks/specfs_bench/data/code/interface-util/check_open.c
@@ -0,0 +1,18 @@
+#include "interface-util.h"
+
+int check_open(struct inode *inum, unsigned mode) {
+    int result = 1;
+
+    if (inum != NULL) {
+        int inum_is_dir = (inum->mode == DIR_MODE);
+        int mode_is_dir = (mode == DIR_MODE);
+
+        if (inum_is_dir == mode_is_dir) {
+            result = 0;
+        }
+
+        unlock(inum);
+    }
+
+    return result;
+}
\ No newline at end of file
diff --git a/benchmarks/specfs_bench/data/code/interface-util/check_src_exist_dst_delete.c b/benchmarks/specfs_bench/data/code/interface-util/check_src_exist_dst_delete.c
new file mode 100644
index 00000000..98003c31
--- /dev/null
+++ b/benchmarks/specfs_bench/data/code/interface-util/check_src_exist_dst_delete.c
@@ -0,0 +1,68 @@
+#include "interface-util.h"
+
+int check_src_exist_dst_delete(struct inode *srcdir, struct inode *dstdir, char *srcname, char *dstname) {
+    struct inode *srcinode = NULL;
+    struct inode *dstinode = NULL;
+    
+    // Find srcinode
+    srcinode = inode_find(srcdir, srcname);
+    if (srcinode == NULL) {
+        unlock2dir(srcdir, dstdir);
+        return 1;
+    }
+    
+    // Check dstdir validity
+    if (dstdir->mode != DIR_MODE || dstdir->size >= MAX_DIR_SIZE) {
+        unlock2dir(srcdir, dstdir);
+        return 1;
+    }
+    
+    // Check if dstinode exists
+    dstinode = inode_find(dstdir, dstname);
+    
+    if (dstinode != NULL) {
+        // Acquire locks for srcinode and dstinode
+        // Handle case where srcinode == dstinode to avoid double-locking
+        if (srcinode == dstinode) {
+            lock(srcinode);
+        } else {
+            lock(srcinode);
+            lock(dstinode);
+        }
+        
+        // Check if same inode
+        if (srcinode != dstinode) {
+            // Check type compatibility
+            int src_is_dir = (srcinode->mode == DIR_MODE);
+            int dst_is_dir = (dstinode->mode == DIR_MODE);
+            
+            if (src_is_dir != dst_is_dir) {
+                unlock(srcinode);
+                unlock(dstinode);
+                unlock2dir(srcdir, dstdir);
+                return 1;
+            }
+            
+            // If dstinode is directory, check it's empty
+            if (dst_is_dir && dstinode->size != 0) {
+                unlock(srcinode);
+                unlock(dstinode);
+                unlock2dir(srcdir, dstdir);
+                return 1;
+            }
+        }
+        
+        // Release srcinode lock, keep dstinode lock
+        // If srcinode == dstinode, do NOT unlock (dstinode lock must remain held)
+        if (srcinode != dstinode) {
+            unlock(srcinode);
+        }
+        // dstinode lock remains held
+    } else {
+        // No dstinode, no additional checks needed
+        // srcinode was never locked, so nothing to unlock
+    }
+    
+    // Success - srcdir and dstdir locks remain held
+    return 0;
+}
\ No newline at end of file
diff --git a/benchmarks/specfs_bench/data/code/interface-util/check_unlock.c b/benchmarks/specfs_bench/data/code/interface-util/check_unlock.c
new file mode 100644
index 00000000..feeb72cd
--- /dev/null
+++ b/benchmarks/specfs_bench/data/code/interface-util/check_unlock.c
@@ -0,0 +1,7 @@
+#include "interface-util.h"
+
+void check_unlock(struct inode* parent, struct inode* src, struct inode* dst) {
+    if (parent != src && parent != dst) {
+        unlock(parent);
+    }
+}
\ No newline at end of file
diff --git a/benchmarks/specfs_bench/data/code/interface/atomfs_del.c b/benchmarks/specfs_bench/data/code/interface/atomfs_del.c
new file mode 100644
index 00000000..2dee70f5
--- /dev/null
+++ b/benchmarks/specfs_bench/data/code/interface/atomfs_del.c
@@ -0,0 +1,36 @@
+#include "interface.h"
+
+int atomfs_del(char* path[], char* name) {
+    struct inode *parent;
+    
+    // Lock root and traverse to parent directory
+    lock(root_inum);
+    parent = locate(root_inum, path);
+    
+    // If path traversal failed, return error (locate already released all locks)
+    if (parent == NULL) {
+        return -1;
+    }
+    
+    // Check if deletion is allowed
+    // If check_del returns 0, parent lock is still held
+    // If check_del returns non-zero, parent lock is released
+    int del_check = check_del(parent, name);
+    if (del_check != 0) {
+        // check_del already released the lock on failure
+        return -1;
+    }
+    
+    // Delete the inode (parent still locked from check_del success)
+    struct inode *deleted = inode_delete(parent, name);
+    
+    // Dispose of the deleted inode if successful
+    if (deleted != NULL) {
+        dispose_inode(deleted);
+    }
+    
+    // Release parent lock (check_del succeeded, so lock was still held)
+    unlock(parent);
+    
+    return 0;
+}
\ No newline at end of file
diff --git a/benchmarks/specfs_bench/data/code/interface/atomfs_getattr.c b/benchmarks/specfs_bench/data/code/interface/atomfs_getattr.c
new file mode 100644
index 00000000..70d0bb98
--- /dev/null
+++ b/benchmarks/specfs_bench/data/code/interface/atomfs_getattr.c
@@ -0,0 +1,22 @@
+#include "interface.h"
+
+extern struct inode* root_inum;
+
+struct getattr_ret* atomfs_getattr(char* path[]) {
+    struct inode* target;
+    struct getattr_ret* ret;
+    
+    lock(root_inum);
+    
+    target = locate(root_inum, path);
+    
+    if (target == NULL) {
+        return NULL;
+    }
+    
+    ret = malloc_getattr_ret(target, target->mode, target->size, target->maj, target->min);
+    
+    unlock(target);
+    
+    return ret;
+}
\ No newline at end of file
diff --git a/benchmarks/specfs_bench/data/code/interface/atomfs_ins.c b/benchmarks/specfs_bench/data/code/interface/atomfs_ins.c
new file mode 100644
index 00000000..c5159f7d
--- /dev/null
+++ b/benchmarks/specfs_bench/data/code/interface/atomfs_ins.c
@@ -0,0 +1,37 @@
+#include "interface.h"
+
+int atomfs_ins(char* path[], char* name, int mode, unsigned maj, unsigned min) {
+    struct inode *cur;
+    
+    // Lock root_inum before starting traversal
+    lock(root_inum);
+    
+    // Traverse the path to find the target directory
+    cur = locate(root_inum, path);
+    
+    // If locate returns NULL, all locks are released, return failure
+    if (cur == NULL) {
+        return -1;
+    }
+    
+    // Check if insertion is possible
+    if (check_ins(cur, name) != 0) {
+        // check_ins releases lock if it returns non-zero
+        return -1;
+    }
+    
+    // At this point, cur is still locked (check_ins returned 0)
+    // Allocate new inode
+    struct inode *new_inode = malloc_inode(mode, maj, min);
+    
+    // Insert the new inode into the directory
+    if (inode_insert(cur, new_inode, name) != 0) {
+        unlock(cur);
+        return -1;
+    }
+    
+    // Release the lock on cur before returning
+    unlock(cur);
+    
+    return 0;
+}
\ No newline at end of file
diff --git a/benchmarks/specfs_bench/data/code/interface/atomfs_open.c b/benchmarks/specfs_bench/data/code/interface/atomfs_open.c
new file mode 100644
index 00000000..171f6f94
--- /dev/null
+++ b/benchmarks/specfs_bench/data/code/interface/atomfs_open.c
@@ -0,0 +1,18 @@
+#include "interface.h"
+
+struct inode *atomfs_open(char *path[], unsigned mode) {
+    struct inode *target;
+    
+    lock(root_inum);
+    target = locate(root_inum, path);
+    
+    if (target == NULL) {
+        return NULL;
+    }
+    
+    if (check_open(target, mode) != 0) {
+        return NULL;
+    }
+    
+    return target;
+}
\ No newline at end of file
diff --git a/benchmarks/specfs_bench/data/code/interface/atomfs_read.c b/benchmarks/specfs_bench/data/code/interface/atomfs_read.c
new file mode 100644
index 00000000..5f761336
--- /dev/null
+++ b/benchmarks/specfs_bench/data/code/interface/atomfs_read.c
@@ -0,0 +1,17 @@
+#include "interface.h"
+
+struct read_ret* atomfs_read(char* path[], unsigned size, unsigned offset) {
+    struct inode *inum;
+    
+    lock(root_inum);
+    inum = locate(root_inum, path);
+    
+    if (inum == NULL || check_file(inum) != 0) {
+        return NULL;
+    }
+    
+    struct read_ret *result = inode_read(inum, size, offset);
+    unlock(inum);
+    
+    return result;
+}
\ No newline at end of file
diff --git a/benchmarks/specfs_bench/data/code/interface/atomfs_readdir.c b/benchmarks/specfs_bench/data/code/interface/atomfs_readdir.c
new file mode 100644
index 00000000..553ed40d
--- /dev/null
+++ b/benchmarks/specfs_bench/data/code/interface/atomfs_readdir.c
@@ -0,0 +1,41 @@
+#include "interface.h"
+
+char **atomfs_readdir(char *path[]) {
+    struct inode *target = NULL;
+    char **dircontent = NULL;
+
+    // Lock root_inum before calling locate (as per locate's pre-condition)
+    lock(root_inum);
+
+    // Locate the inode; if successful, the lock on 'target' is acquired.
+    target = locate(root_inum, path);
+
+    // Case 2a: Path traversal failed.
+    if (target == NULL) {
+        // locate already released all locks including root_inum
+        return NULL;
+    }
+
+    // Check if 'target' is a directory.
+    // If check_dir returns non-zero, it releases the lock on 'target'.
+    if (check_dir(target) != 0) {
+        return NULL;
+    }
+
+    // Allocate memory for directory content (size + 1 for NULL termination).
+    dircontent = malloc_dir_content(target->size + 1);
+
+    // Handle allocation failure.
+    if (dircontent == NULL) {
+        unlock(target);
+        return NULL;
+    }
+
+    // Fill the directory content.
+    fill_dir(target, dircontent);
+
+    // Post-condition: No lock is held. Release the lock on 'target'.
+    unlock(target);
+
+    return dircontent;
+}
\ No newline at end of file
diff --git a/benchmarks/specfs_bench/data/code/interface/atomfs_rename.c b/benchmarks/specfs_bench/data/code/interface/atomfs_rename.c
new file mode 100644
index 00000000..c70a7000
--- /dev/null
+++ b/benchmarks/specfs_bench/data/code/interface/atomfs_rename.c
@@ -0,0 +1,141 @@
+#include "interface.h"
+
+int atomfs_rename(char* srcpath[], char* dstpath[], char* srcname, char* dstname) {
+    int ret = -1;
+    struct inode* srcdir = NULL;
+    struct inode* dstdir = NULL;
+    int src_suffix_len = 0;
+    int dst_suffix_len = 0;
+    char** src_suffix = NULL;
+    char** dst_suffix = NULL;
+
+    // Phase 1: Traverse Common Path
+    lock(root_inum);
+    
+    char** common = calculate(srcpath, dstpath);
+    if (common == NULL) {
+        unlock(root_inum);
+        goto cleanup;
+    }
+    
+    int common_len = getlen(common);
+    
+    struct inode* parent = locate(root_inum, common);
+    free_path(common);
+    
+    if (parent == NULL) {
+        // locate() releases all locks when returning NULL
+        goto cleanup;
+    }
+    
+    // Phase 2: Traverse Remaining Paths
+    int src_len = getlen(srcpath);
+    int dst_len = getlen(dstpath);
+    src_suffix_len = src_len - common_len;
+    dst_suffix_len = dst_len - common_len;
+    
+    // Allocate and copy src suffix
+    src_suffix = malloc(sizeof(char*) * (src_suffix_len + 1));
+    if (src_suffix == NULL) {
+        check_unlock(parent, NULL, NULL);
+        goto cleanup;
+    }
+    for (int i = 0; i < src_suffix_len; i++) {
+        src_suffix[i] = strdup(srcpath[common_len + i]);
+        if (src_suffix[i] == NULL) {
+            for (int j = 0; j < i; j++) {
+                free(src_suffix[j]);
+            }
+            free(src_suffix);
+            src_suffix = NULL;
+            check_unlock(parent, NULL, NULL);
+            goto cleanup;
+        }
+    }
+    src_suffix[src_suffix_len] = NULL;
+    
+    // Allocate and copy dst suffix
+    dst_suffix = malloc(sizeof(char*) * (dst_suffix_len + 1));
+    if (dst_suffix == NULL) {
+        for (int i = 0; i < src_suffix_len; i++) {
+            free(src_suffix[i]);
+        }
+        free(src_suffix);
+        src_suffix = NULL;
+        check_unlock(parent, NULL, NULL);
+        goto cleanup;
+    }
+    for (int i = 0; i < dst_suffix_len; i++) {
+        dst_suffix[i] = strdup(dstpath[common_len + i]);
+        if (dst_suffix[i] == NULL) {
+            for (int j = 0; j < i; j++) {
+                free(dst_suffix[j]);
+            }
+            free(dst_suffix);
+            dst_suffix = NULL;
+            for (int j = 0; j < src_suffix_len; j++) {
+                free(src_suffix[j]);
+            }
+            free(src_suffix);
+            src_suffix = NULL;
+            check_unlock(parent, NULL, NULL);
+            goto cleanup;
+        }
+    }
+    dst_suffix[dst_suffix_len] = NULL;
+    
+    // Find srcdir from parent
+    srcdir = locate_hold(parent, src_suffix);
+    if (srcdir == NULL) {
+        check_unlock(parent, NULL, NULL);
+        goto cleanup;
+    }
+    
+    // Find dstdir from parent
+    dstdir = locate_hold(parent, dst_suffix);
+    if (dstdir == NULL) {
+        check_unlock(parent, srcdir, NULL);
+        unlock(srcdir);
+        goto cleanup;
+    }
+    
+    // Release parent lock if different from srcdir/dstdir
+    check_unlock(parent, srcdir, dstdir);
+    
+    // Phase 3: Checks and Operations
+    if (check_src_exist_dst_delete(srcdir, dstdir, srcname, dstname) != 0) {
+        goto cleanup;
+    }
+    
+    // Perform rename operation
+    struct inode* srcinode = inode_delete(srcdir, srcname);
+    struct inode* dstinode = inode_delete(dstdir, dstname);
+    
+    if (dstinode != NULL) {
+        dispose_inode(dstinode);
+    }
+    
+    // Fixed: Use srcinode instead of srcdir
+    inode_insert(dstdir, srcinode, dstname);
+    
+    // Release locks
+    unlock2dir(srcdir, dstdir);
+    
+    ret = 0;
+
+cleanup:
+    if (src_suffix != NULL) {
+        for (int i = 0; i < src_suffix_len; i++) {
+            free(src_suffix[i]);
+        }
+        free(src_suffix);
+    }
+    if (dst_suffix != NULL) {
+        for (int i = 0; i < dst_suffix_len; i++) {
+            free(dst_suffix[i]);
+        }
+        free(dst_suffix);
+    }
+    
+    return ret;
+}
\ No newline at end of file
diff --git a/benchmarks/specfs_bench/data/code/interface/atomfs_truncate.c b/benchmarks/specfs_bench/data/code/interface/atomfs_truncate.c
new file mode 100644
index 00000000..183da401
--- /dev/null
+++ b/benchmarks/specfs_bench/data/code/interface/atomfs_truncate.c
@@ -0,0 +1,32 @@
+#include "interface.h"
+
+int atomfs_truncate(char* path[], unsigned offset) {
+    struct inode *target;
+    
+    // Check if offset exceeds maximum file size
+    if (offset > MAX_FILE_SIZE) {
+        return -1;
+    }
+    
+    // Lock root and locate the target inode
+    lock(root_inum);
+    target = locate(root_inum, path);
+    
+    // If path traversal failed, return error
+    if (target == NULL) {
+        return -1;
+    }
+    
+    // Verify it's a regular file
+    // Note: check_file releases lock on failure, keeps lock on success
+    if (check_file(target) != 0) {
+        return -1;
+    }
+    
+    // Truncate the file (inode_truncate keeps lock)
+    inode_truncate(target, offset);
+    
+    // Release lock and return success
+    unlock(target);
+    return 0;
+}
\ No newline at end of file
diff --git a/benchmarks/specfs_bench/data/code/interface/atomfs_write.c b/benchmarks/specfs_bench/data/code/interface/atomfs_write.c
new file mode 100644
index 00000000..bc6f186d
--- /dev/null
+++ b/benchmarks/specfs_bench/data/code/interface/atomfs_write.c
@@ -0,0 +1,34 @@
+#include "interface.h"
+
+int atomfs_write(char* path[], const char* buf, unsigned size, unsigned offset) {
+    struct inode *inum;
+
+    // Pre-condition: no lock is owned.
+    // locate requires cur (root_inum) to be locked.
+    lock(root_inum);
+
+    // locate releases root_inum lock and acquires inum lock if found.
+    // If not found, all locks are released.
+    inum = locate(root_inum, path);
+
+    if (inum == NULL) {
+        // locate released all locks.
+        return -1;
+    }
+
+    // check_file expects inum to be locked if not NULL.
+    // Returns 1 if not writable, releasing the lock.
+    // Returns 0 if writable, keeping the lock.
+    if (check_file(inum) == 1) {
+        // check_file released the lock on failure.
+        return -1;
+    }
+
+    // check_file returned 0, inum is still locked.
+    unsigned written = inode_write(inum, buf, size, offset);
+
+    // Post-condition: no lock is owned.
+    unlock(inum);
+
+    return written;
+}
\ No newline at end of file
diff --git a/benchmarks/specfs_bench/data/code/path/locate.c b/benchmarks/specfs_bench/data/code/path/locate.c
new file mode 100644
index 00000000..2492b758
--- /dev/null
+++ b/benchmarks/specfs_bench/data/code/path/locate.c
@@ -0,0 +1,34 @@
+#include "path.h"
+
+struct inode* locate(struct inode* cur, char* path[]) {
+    struct inode* current = cur;
+    
+    // Handle empty path case
+    if (path[0] == NULL) {
+        return current;
+    }
+    
+    // Iterate through path components
+    for (int i = 0; path[i] != NULL; i++) {
+        char* name = path[i];
+        
+        // Find next inode (non-locking operation)
+        struct inode* next = inode_find(current, name);
+        
+        // Handle path failure
+        if (next == NULL) {
+            unlock(current);
+            return NULL;
+        }
+        
+        // Lock coupling: acquire next lock before releasing current
+        lock(next);
+        unlock(current);
+        
+        // Advance to next node
+        current = next;
+    }
+    
+    // Successfully traversed entire path, current is locked
+    return current;
+}
\ No newline at end of file
diff --git a/benchmarks/specfs_bench/data/code/path/locate_hold.c b/benchmarks/specfs_bench/data/code/path/locate_hold.c
new file mode 100644
index 00000000..53d9ac2d
--- /dev/null
+++ b/benchmarks/specfs_bench/data/code/path/locate_hold.c
@@ -0,0 +1,17 @@
+#include "path.h"
+
+struct inode* locate_hold(struct inode *cur, char *path[]) {
+    if (path[0] == NULL) {
+        return cur;
+    }
+    
+    struct inode *next = inode_find(cur, path[0]);
+    
+    if (next == NULL) {
+        return NULL;
+    }
+    
+    lock(next);
+    
+    return locate(next, &path[1]);
+}
\ No newline at end of file
diff --git a/benchmarks/specfs_bench/data/code/util/calculate.c b/benchmarks/specfs_bench/data/code/util/calculate.c
new file mode 100644
index 00000000..72f2338b
--- /dev/null
+++ b/benchmarks/specfs_bench/data/code/util/calculate.c
@@ -0,0 +1,28 @@
+#include "util.h"
+
+char** calculate(char* srcpath[], char* dstpath[]) {
+    unsigned i = 0;
+    while (srcpath[i] != NULL && dstpath[i] != NULL) {
+        const char *s = srcpath[i];
+        const char *d = dstpath[i];
+        while (*s == *d) {
+            if (*s == '\0') {
+                break;
+            }
+            s++;
+            d++;
+        }
+        if (*s != *d) {
+            break;
+        }
+        i++;
+    }
+
+    char** compath = malloc_path(i + 1);
+    for (unsigned j = 0; j < i; j++) {
+        compath[j] = malloc_string(srcpath[j]);
+    }
+    compath[i] = NULL;
+
+    return compath;
+}
\ No newline at end of file
diff --git a/benchmarks/specfs_bench/data/code/util/dispose_inode.c b/benchmarks/specfs_bench/data/code/util/dispose_inode.c
new file mode 100644
index 00000000..030bc23c
--- /dev/null
+++ b/benchmarks/specfs_bench/data/code/util/dispose_inode.c
@@ -0,0 +1,40 @@
+#include "util.h"
+
+void dispose_inode(struct inode* inum) {
+    if (inum == NULL) {
+        return;
+    }
+
+    // Destroy the mutex associated with the inode
+    if (inum->impl != NULL) {
+        mcs_mutex_destroy(inum->impl);
+    }
+
+    // Remove inode contents based on mode
+    if (inum->mode == DIR_MODE && inum->dir != NULL) {
+        struct dirtb *dt = inum->dir;
+        for (int i = 0; i < DIRTB_NUM; i++) {
+            struct entry *e = dt->tb[i];
+            while (e != NULL) {
+                struct entry *next = e->next;
+                if (e->name != NULL) {
+                    free(e->name);
+                }
+                free(e);
+                e = next;
+            }
+        }
+        free(dt);
+    } else if (inum->mode == FILE_MODE && inum->file != NULL) {
+        struct indextb *ft = inum->file;
+        for (int i = 0; i < INDEXTB_NUM; i++) {
+            if (ft->index[i] != NULL) {
+                free(ft->index[i]);
+            }
+        }
+        free(ft);
+    }
+
+    // Free the inode structure itself
+    free(inum);
+}
\ No newline at end of file
diff --git a/benchmarks/specfs_bench/data/code/util/fill_dir.c b/benchmarks/specfs_bench/data/code/util/fill_dir.c
new file mode 100644
index 00000000..41af8730
--- /dev/null
+++ b/benchmarks/specfs_bench/data/code/util/fill_dir.c
@@ -0,0 +1,17 @@
+#include "util.h"
+
+void fill_dir(struct inode* inum, char** dircontent) {
+    int i = 0;
+    int j = 0;
+    struct entry *walk;
+
+    for (i = 0; i < DIRTB_NUM; i++) {
+        walk = inum->dir->tb[i];
+        while (walk != NULL) {
+            dircontent[j] = malloc_string(walk->name);
+            j++;
+            walk = walk->next;
+        }
+    }
+    dircontent[j] = NULL;
+}
\ No newline at end of file
diff --git a/benchmarks/specfs_bench/data/code/util/free_dirs.c b/benchmarks/specfs_bench/data/code/util/free_dirs.c
new file mode 100644
index 00000000..02c2cb2a
--- /dev/null
+++ b/benchmarks/specfs_bench/data/code/util/free_dirs.c
@@ -0,0 +1,9 @@
+#include "util.h"
+
+void free_dirs(char *dirname[]) {
+    int i = 0;
+    while (dirname[i] != NULL) {
+        free(dirname[i]);
+        i++;
+    }
+}
\ No newline at end of file
diff --git a/benchmarks/specfs_bench/data/code/util/free_entry.c b/benchmarks/specfs_bench/data/code/util/free_entry.c
new file mode 100644
index 00000000..23aac27f
--- /dev/null
+++ b/benchmarks/specfs_bench/data/code/util/free_entry.c
@@ -0,0 +1,6 @@
+#include "util.h"
+
+void free_entry(struct entry* en) {
+	free(en->name);
+	free(en);
+}
\ No newline at end of file
diff --git a/benchmarks/specfs_bench/data/code/util/free_path.c b/benchmarks/specfs_bench/data/code/util/free_path.c
new file mode 100644
index 00000000..4a231a19
--- /dev/null
+++ b/benchmarks/specfs_bench/data/code/util/free_path.c
@@ -0,0 +1,13 @@
+#include "util.h"
+
+void free_path(char** path) {
+    if (path == NULL) {
+        return;
+    }
+
+    for (int i = 0; path[i] != NULL; i++) {
+        free(path[i]);
+    }
+
+    free(path);
+}
\ No newline at end of file
diff --git a/benchmarks/specfs_bench/data/code/util/free_readret.c b/benchmarks/specfs_bench/data/code/util/free_readret.c
new file mode 100644
index 00000000..ca70016e
--- /dev/null
+++ b/benchmarks/specfs_bench/data/code/util/free_readret.c
@@ -0,0 +1,6 @@
+#include "util.h"
+
+void free_readret(struct read_ret *p) {
+    free(p->buf);
+    free(p);
+}
\ No newline at end of file
diff --git a/benchmarks/specfs_bench/data/code/util/getlen.c b/benchmarks/specfs_bench/data/code/util/getlen.c
new file mode 100644
index 00000000..948de217
--- /dev/null
+++ b/benchmarks/specfs_bench/data/code/util/getlen.c
@@ -0,0 +1,9 @@
+#include "util.h"
+
+int getlen(char* path[]) {
+    int count = 0;
+    while (path[count] != NULL) {
+        count++;
+    }
+    return count;
+}
\ No newline at end of file
diff --git a/benchmarks/specfs_bench/data/code/util/hash_name.c b/benchmarks/specfs_bench/data/code/util/hash_name.c
new file mode 100644
index 00000000..ca466c37
--- /dev/null
+++ b/benchmarks/specfs_bench/data/code/util/hash_name.c
@@ -0,0 +1,16 @@
+#include "util.h"
+
+unsigned int hash_name(char* name) {
+    unsigned int hash = 0;
+
+    if (name == NULL) {
+        return 0;
+    }
+
+    while (*name != '\0') {
+        hash = (hash * 131) + *name;
+        name++;
+    }
+
+    return hash & 0x1ff;
+}
\ No newline at end of file
diff --git a/benchmarks/specfs_bench/data/code/util/lock.c b/benchmarks/specfs_bench/data/code/util/lock.c
new file mode 100644
index 00000000..85043e59
--- /dev/null
+++ b/benchmarks/specfs_bench/data/code/util/lock.c
@@ -0,0 +1,8 @@
+#include "util.h"
+
+void lock(struct inode* inum) {
+    mcs_node_t *me = (mcs_node_t *)malloc(sizeof(mcs_node_t));
+    mcs_mutex_lock(inum->impl, me);
+    inum->hd = me;
+    inum->mutex = syscall(SYS_gettid);
+}
\ No newline at end of file
diff --git a/benchmarks/specfs_bench/data/code/util/malloc_buffer.c b/benchmarks/specfs_bench/data/code/util/malloc_buffer.c
new file mode 100644
index 00000000..24c52d93
--- /dev/null
+++ b/benchmarks/specfs_bench/data/code/util/malloc_buffer.c
@@ -0,0 +1,5 @@
+#include "util.h"
+
+char* malloc_buffer(unsigned len) {
+    return (char*)malloc(len);
+}
\ No newline at end of file
diff --git a/benchmarks/specfs_bench/data/code/util/malloc_dir_content.c b/benchmarks/specfs_bench/data/code/util/malloc_dir_content.c
new file mode 100644
index 00000000..e0871dbe
--- /dev/null
+++ b/benchmarks/specfs_bench/data/code/util/malloc_dir_content.c
@@ -0,0 +1,5 @@
+#include "util.h"
+
+char** malloc_dir_content(unsigned size) {
+    return (char**)malloc(size * sizeof(char*));
+}
\ No newline at end of file
diff --git a/benchmarks/specfs_bench/data/code/util/malloc_entry.c b/benchmarks/specfs_bench/data/code/util/malloc_entry.c
new file mode 100644
index 00000000..305ec891
--- /dev/null
+++ b/benchmarks/specfs_bench/data/code/util/malloc_entry.c
@@ -0,0 +1,5 @@
+#include "util.h"
+
+struct entry *malloc_entry() {
+    return malloc(sizeof(struct entry));
+}
\ No newline at end of file
diff --git a/benchmarks/specfs_bench/data/code/util/malloc_getattr_ret.c b/benchmarks/specfs_bench/data/code/util/malloc_getattr_ret.c
new file mode 100644
index 00000000..52bc946c
--- /dev/null
+++ b/benchmarks/specfs_bench/data/code/util/malloc_getattr_ret.c
@@ -0,0 +1,21 @@
+#include "util.h"
+
+struct getattr_ret* malloc_getattr_ret(struct inode* inum, unsigned mode, unsigned size, unsigned maj, unsigned min) {
+    struct getattr_ret* ret = malloc(sizeof(struct getattr_ret));
+    if (ret == NULL) {
+        return NULL;
+    }
+
+    ret->inum = inum;
+    ret->mode = mode;
+    ret->size = size;
+    ret->maj = maj;
+    ret->min = min;
+
+    if (mode == DIR_MODE) {
+        ret->maj = 0;
+        ret->min = 0;
+    }
+
+    return ret;
+}
\ No newline at end of file
diff --git a/benchmarks/specfs_bench/data/code/util/malloc_inode.c b/benchmarks/specfs_bench/data/code/util/malloc_inode.c
new file mode 100644
index 00000000..fa8fbb76
--- /dev/null
+++ b/benchmarks/specfs_bench/data/code/util/malloc_inode.c
@@ -0,0 +1,29 @@
+#include "util.h"
+
+struct inode* malloc_inode(int mode, unsigned maj, unsigned min) {
+    struct inode *ino = malloc(sizeof(struct inode));
+    if (ino == NULL) {
+        return NULL;
+    }
+
+    memset(ino, 0, sizeof(struct inode));
+
+    ino->mode = mode;
+    ino->maj = maj;
+    ino->min = min;
+    ino->impl = mcs_mutex_create();
+
+    if (mode == DIR_MODE) {
+        ino->dir = malloc(sizeof(struct dirtb));
+        if (ino->dir != NULL) {
+            memset(ino->dir, 0, sizeof(struct dirtb));
+        }
+    } else {
+        ino->file = malloc(sizeof(struct indextb));
+        if (ino->file != NULL) {
+            memset(ino->file, 0, sizeof(struct indextb));
+        }
+    }
+
+    return ino;
+}
\ No newline at end of file
diff --git a/benchmarks/specfs_bench/data/code/util/malloc_page.c b/benchmarks/specfs_bench/data/code/util/malloc_page.c
new file mode 100644
index 00000000..85f48e8e
--- /dev/null
+++ b/benchmarks/specfs_bench/data/code/util/malloc_page.c
@@ -0,0 +1,5 @@
+#include "util.h"
+
+unsigned char* malloc_page() {
+    return (unsigned char*)calloc(1, PAGE_SIZE);
+}
\ No newline at end of file
diff --git a/benchmarks/specfs_bench/data/code/util/malloc_path.c b/benchmarks/specfs_bench/data/code/util/malloc_path.c
new file mode 100644
index 00000000..968f440c
--- /dev/null
+++ b/benchmarks/specfs_bench/data/code/util/malloc_path.c
@@ -0,0 +1,6 @@
+#include "util.h"
+
+char** malloc_path(unsigned len) {
+    char** paths = calloc(len, sizeof(char*));
+    return paths;
+}
\ No newline at end of file
diff --git a/benchmarks/specfs_bench/data/code/util/malloc_readret.c b/benchmarks/specfs_bench/data/code/util/malloc_readret.c
new file mode 100644
index 00000000..e25e496e
--- /dev/null
+++ b/benchmarks/specfs_bench/data/code/util/malloc_readret.c
@@ -0,0 +1,10 @@
+#include "util.h"
+
+struct read_ret* malloc_readret() {
+    struct read_ret* ptr = malloc(sizeof(struct read_ret));
+    if (ptr != NULL) {
+        ptr->buf = NULL;
+        ptr->num = 0;
+    }
+    return ptr;
+}
\ No newline at end of file
diff --git a/benchmarks/specfs_bench/data/code/util/malloc_string.c b/benchmarks/specfs_bench/data/code/util/malloc_string.c
new file mode 100644
index 00000000..8674ea9c
--- /dev/null
+++ b/benchmarks/specfs_bench/data/code/util/malloc_string.c
@@ -0,0 +1,8 @@
+#include "util.h"
+
+char* malloc_string(const char* name) {
+    size_t len = strlen(name);
+    char* str = malloc(len + 1);
+    strcpy(str, name);
+    return str;
+}
\ No newline at end of file
diff --git a/benchmarks/specfs_bench/data/code/util/split_dirs.c b/benchmarks/specfs_bench/data/code/util/split_dirs.c
new file mode 100644
index 00000000..b7f73c19
--- /dev/null
+++ b/benchmarks/specfs_bench/data/code/util/split_dirs.c
@@ -0,0 +1,18 @@
+#include "util.h"
+
+void split_dirs(const char *path, char *dirname[]) {
+    char *temp = malloc_string(path);
+    char *saveptr;
+    char *token;
+    int i = 0;
+
+    token = strtok_r(temp, "/", &saveptr);
+    while (token != NULL) {
+        assert(i < MAX_PATH_LEN);
+        assert(strlen(token) <= MAX_FILE_LEN);
+        dirname[i] = malloc_string(token);
+        i++;
+        token = strtok_r(NULL, "/", &saveptr);
+    }
+    free(temp);
+}
\ No newline at end of file
diff --git a/benchmarks/specfs_bench/data/code/util/split_dirs_file.c b/benchmarks/specfs_bench/data/code/util/split_dirs_file.c
new file mode 100644
index 00000000..0b47d2ad
--- /dev/null
+++ b/benchmarks/specfs_bench/data/code/util/split_dirs_file.c
@@ -0,0 +1,65 @@
+#include "util.h"
+
+void split_dirs_file(const char *path, char *dirname[], char *filename) {
+    // Check for NULL or empty path
+    if (path == NULL || path[0] == '\0') {
+        return;
+    }
+    
+    // Create a mutable copy of the path
+    char *path_copy = malloc_string(path);
+    if (path_copy == NULL) {
+        return;
+    }
+    
+    // Initialize variables for tokenization
+    char *token;
+    char *saveptr;
+    int token_count = 0;
+    
+    // Temporary storage for all tokens
+    char *tokens[MAX_PATH_LEN];
+    
+    // Tokenize the path by '/'
+    token = strtok_r(path_copy, "/", &saveptr);
+    
+    while (token != NULL && token_count < MAX_PATH_LEN) {
+        tokens[token_count] = malloc_string(token);
+        if (tokens[token_count] == NULL) {
+            // Handle allocation failure - clean up what we have
+            for (int i = 0; i < token_count; i++) {
+                free(tokens[i]);
+            }
+            free(path_copy);
+            return;
+        }
+        token_count++;
+        token = strtok_r(NULL, "/", &saveptr);
+    }
+    
+    // If no tokens found, cleanup and return
+    if (token_count == 0) {
+        free(path_copy);
+        return;
+    }
+    
+    // Last token is the filename
+    strncpy(filename, tokens[token_count - 1], MAX_FILE_LEN - 1);
+    filename[MAX_FILE_LEN - 1] = '\0';
+    
+    // All previous tokens are directories
+    for (int i = 0; i < token_count - 1; i++) {
+        dirname[i] = tokens[i];
+    }
+    
+    // Set the entry after last directory to NULL
+    if (token_count > 1) {
+        dirname[token_count - 1] = NULL;
+    }
+    
+    // Free the last token (it was copied to filename)
+    free(tokens[token_count - 1]);
+    
+    // Clean up the temporary path copy
+    free(path_copy);
+}
\ No newline at end of file
diff --git a/benchmarks/specfs_bench/data/code/util/unlock.c b/benchmarks/specfs_bench/data/code/util/unlock.c
new file mode 100644
index 00000000..1f08a80c
--- /dev/null
+++ b/benchmarks/specfs_bench/data/code/util/unlock.c
@@ -0,0 +1,8 @@
+#include "util.h"
+
+void unlock(struct inode* inum) {
+    struct mcs_node *me = inum->hd;
+    inum->mutex = 0;
+    mcs_mutex_unlock(inum->impl, me);
+    free(me);
+}
\ No newline at end of file
diff --git a/benchmarks/specfs_bench/data/code/util/unlock2dir.c b/benchmarks/specfs_bench/data/code/util/unlock2dir.c
new file mode 100644
index 00000000..fdbdec66
--- /dev/null
+++ b/benchmarks/specfs_bench/data/code/util/unlock2dir.c
@@ -0,0 +1,10 @@
+#include "util.h"
+
+void unlock2dir (struct inode* srcdir, struct inode* dstdir) {
+    if (srcdir == dstdir) {
+        unlock(srcdir);
+    } else {
+        unlock(srcdir);
+        unlock(dstdir);
+    }
+}
\ No newline at end of file
diff --git a/benchmarks/specfs_bench/data/spec/file/file_allocate.spec b/benchmarks/specfs_bench/data/spec/file/file_allocate.spec
new file mode 100644
index 00000000..ec2661cd
--- /dev/null
+++ b/benchmarks/specfs_bench/data/spec/file/file_allocate.spec
@@ -0,0 +1,50 @@
+[PROMPT]
+Provide complete `file_allocate.c` file that implement `file_allocate` operation. You can use information from [RELY], [GUARANTEE] and [SPECIFICATION] as described below. Only provide the implementation of that single function and only include `file.h` as the header. Your output is wrapped in a C code block, and no other unrelavent code should be given.
+
+[RELY]
+```c
+unsigned char* malloc_page();
+```
+```c
+typedef struct indextb {
+	unsigned char *index[INDEXTB_NUM];
+} indextb;
+```
+```c
+#define PG_SIZE 4096
+#define INDEXTB_NUM 8192
+#define DIRTB_NUM 512
+#define MAX_FILE_LEN 256
+#define MAX_DIR_SIZE 10000000
+#define MAX_PATH_LEN 100
+#define MAX_FILE_SIZE ((unsigned)(INDEXTB_NUM * PG_SIZE))
+#define PAGE_SIZE (4096)
+```
+```c
+typedef struct inode {
+	int mutex;
+	struct mcs_mutex *impl;
+	struct mcs_node *hd;
+	unsigned maj;
+	unsigned min;
+	unsigned int mode;
+	unsigned int size;
+	struct dirtb *dir;
+	struct indextb *file;
+} inode;
+```
+
+[GUARANTEE]
+```c
+void file_allocate(struct inode *node, unsigned offset, unsigned len);
+```
+
+[SPECIFICATION]
+**Pre-Condition**:
+- The `node` parameter points to a valid `inode` structure, i.e., `tb` is not NULL. The index_num is guarenteed to be within bounds.
+- The `offset` is the offset in the file where the allocation starts.
+- The `len` is the number of bytes to allocate starting from the `offset`.
+**Post-Condition**:
+- Calculate the starting page and the end page, each page is of `PG_SIZE` bytes.
+- Iterate from the starting page to the end page, allocating pages as needed.
+
diff --git a/benchmarks/specfs_bench/data/spec/file/file_clear.spec b/benchmarks/specfs_bench/data/spec/file/file_clear.spec
new file mode 100644
index 00000000..e52ba855
--- /dev/null
+++ b/benchmarks/specfs_bench/data/spec/file/file_clear.spec
@@ -0,0 +1,36 @@
+[PROMPT]
+Provide complete `file_clear.c` file that implement `file_clear` operation. You can use information from [RELY], [GUARANTEE] and [SPECIFICATION] as described below. Only provide the implementation of that single function and only include `file.h` as the header. Your output is wrapped in a C code block, and no other unrelavent code should be given.
+
+[RELY]
+// `file_write` writes a given data buffer (or zeroes if `data` is `NULL`) into a file’s page-indexed storage, handling offsets, page boundaries, and partial writes until the specified length is covered.
+```c
+void file_write(struct inode *node, unsigned offset, unsigned len, const char *data);
+```
+```c
+typedef struct inode {
+	int mutex;
+	struct mcs_mutex *impl;
+	struct mcs_node *hd;
+	unsigned maj;
+	unsigned min;
+	unsigned int mode;
+	unsigned int size;
+	struct dirtb *dir;
+	struct indextb *file;
+} inode;
+```
+
+[GUARANTEE]
+```c
+void file_clear(struct inode *node, unsigned start, unsigned len);
+```
+
+[SPECIFICATION]
+**Pre-Condition**:
+- The `node` parameter points to a valid `inode` structure, i.e., `node` is not NULL.
+- The `start` is the starting offset in the file where the clear operation begins.
+- The `len` is the number of bytes to clear starting from the `start` offset.
+
+**Post-Condition**:
+- The specified range in the file is cleared (set to zero).
+
diff --git a/benchmarks/specfs_bench/data/spec/file/file_read.spec b/benchmarks/specfs_bench/data/spec/file/file_read.spec
new file mode 100644
index 00000000..bec33500
--- /dev/null
+++ b/benchmarks/specfs_bench/data/spec/file/file_read.spec
@@ -0,0 +1,36 @@
+[PROMPT]
+Provide complete `file_read.c` file that implement `file_read` operation. You can use information from [RELY], [GUARANTEE] and [SPECIFICATION] as described below. Only provide the implementation of that single function and only include `file.h` as the header. Your output is wrapped in a C code block, and no other unrelavent code should be given.
+
+[RELY]
+```c
+typedef struct indextb {
+	unsigned char *index[INDEXTB_NUM];
+} indextb;
+```
+```c
+typedef struct inode {
+	int mutex;
+	struct mcs_mutex *impl;
+	struct mcs_node *hd;
+	unsigned maj;
+	unsigned min;
+	unsigned int mode;
+	unsigned int size;
+	struct dirtb *dir;
+	struct indextb *file;
+} inode;
+```
+
+[GUARANTEE]
+```c
+void file_read(struct inode *node, unsigned offset, unsigned len, char *data);
+```
+
+[SPECIFICATION]
+**Pre-Condition**:
+- The `node` parameter points to a valid `inode` structure, i.e., `tb` is not NULL.
+- The requested read range is fully allocated, meaning for every index `i` in the range from `offset >> 12` (inclusive) to the index of the last byte of the read (inclusive), `tb->index[i]` must be non-NULL and point to a valid memory block of size PG_SIZE (4096 bytes).
+- The buffer `data` has `len` bytes allocated.
+**Post-Condition**:
+- The buffer `data` contains the exact `len` bytes from the specified offset. For any valid index i, `tb->index[i]` contains bytes range [i*PG_SIZE+1, (i+1) * PG_SIZE].
+
diff --git a/benchmarks/specfs_bench/data/spec/file/file_write.spec b/benchmarks/specfs_bench/data/spec/file/file_write.spec
new file mode 100644
index 00000000..bd5f2bb5
--- /dev/null
+++ b/benchmarks/specfs_bench/data/spec/file/file_write.spec
@@ -0,0 +1,55 @@
+[PROMPT]
+Provide complete `file_write.c` file that implement `file_write` operation. You can use information from [RELY], [GUARANTEE] and [SPECIFICATION] as described below. Only provide the implementation of that single function and only include `file.h` as the header. Your output is wrapped in a C code block, and no other unrelavent code should be given.
+
+[RELY]
+```c
+#define PG_SIZE 4096
+#define INDEXTB_NUM 8192
+#define DIRTB_NUM 512
+#define MAX_FILE_LEN 256
+#define MAX_DIR_SIZE 10000000
+#define MAX_PATH_LEN 100
+#define MAX_FILE_SIZE ((unsigned)(INDEXTB_NUM * PG_SIZE))
+#define PAGE_SIZE (4096)
+```
+```c
+typedef struct indextb {
+	unsigned char *index[INDEXTB_NUM];
+} indextb;
+```
+```c
+typedef struct inode {
+	int mutex;
+	struct mcs_mutex *impl;
+	struct mcs_node *hd;
+	unsigned maj;
+	unsigned min;
+	unsigned int mode;
+	unsigned int size;
+	struct dirtb *dir;
+	struct indextb *file;
+} inode;
+```
+
+[GUARANTEE]
+```c
+void file_write(struct inode *node, unsigned offset, unsigned len, const char *data);
+```
+
+[SPECIFICATION]
+**Pre-Condition**:
+- `node` is a valid `inode` structure, and its `tb` is a valid pointer, `tb->index` array is sufficiently large to hold all page numbers required for the range [`offset`, `offset + len`). 
+- `offset` and `len` are valid unsigned integers, and `offset + len` does not cause an overflow. 
+- If `data` is not `NULL`, it points to a buffer of at least `len` bytes, and all required pages (derived from the range [`offset`, `offset + len`)) in `tb->index` are already allocated (non-`NULL`).
+
+**Post-Condition**:
+The specified range [`offset`, `offset + len`) is processed as follows:
+
+**Case 1**: `data` is `NULL`  
+- All bytes in the range are initialized to zero. For any page in the range that was unallocated (`tb->index[page]` was `NULL`), the page is allocated, and the relevant portion within the range is zero-initialized. Pages are left unmodified outside the specified range.
+
+**Case 2**: `data` is not `NULL`  
+- The `len` bytes from the `data` buffer are copied into the corresponding positions within the allocated pages of `tb`. All pages in the range are assumed pre-allocated (as per the precondition), and the data is fully written. 
+
+In both cases, the entire `len` bytes are processed, and variables `current_offset` and `remaining` reflect completion (e.g., `remaining == 0`).
+
diff --git a/benchmarks/specfs_bench/data/spec/inode/inode_delete.spec b/benchmarks/specfs_bench/data/spec/inode/inode_delete.spec
new file mode 100644
index 00000000..b76b53eb
--- /dev/null
+++ b/benchmarks/specfs_bench/data/spec/inode/inode_delete.spec
@@ -0,0 +1,51 @@
+[PROMPT]
+Provide complete `inode_delete.c` file that implement `inode_delete` operation. You can use information from [RELY], [GUARANTEE] and [SPECIFICATION] as described below. Only provide the implementation of that single function and only include `inode.h` as the header. Your output is wrapped in a C code block, and no other unrelavent code should be given.
+
+[RELY]
+```c
+unsigned int hash_name(char* name);
+```
+```c
+void free_entry(struct entry* en);
+```
+```c
+typedef struct entry {
+	char *name;
+	void *inum;
+	struct entry *next;
+} entry;
+```
+```c
+typedef struct dirtb {
+	struct entry *tb[DIRTB_NUM];
+} dirtb;
+```
+```c
+typedef struct inode {
+	int mutex;
+	struct mcs_mutex *impl;
+	struct mcs_node *hd;
+	unsigned maj;
+	unsigned min;
+	unsigned int mode;
+	unsigned int size;
+	struct dirtb *dir;
+	struct indextb *file;
+} inode;
+```
+
+[GUARANTEE]
+```c
+struct inode* inode_delete(struct inode* inum, char* name);
+```
+
+[SPECIFICATION]
+**Pre-Condition**:
+there exists an inode pointed to by `cur`. The inode is an directory, i.e., `cur->dir` is not NULL.
+**Post-Condition**:
+there are two cases depending on whether the entry named `name` exists.
+Case1: if an entry named `name` exists in `cur`, the entry is removed from `cur` and freed. The `inum` field of the entry is returned. The `size` of `cur` decreases by 1.
+Case2: if an entry named `name` is not found in `cur`, the return value is NULL.
+
+**Invariant**: 
+**Directory well-formedness**: (1) Each child entry's name is different from others in the same directory. (2) In an inode `inode`, for each name `name`, its entry resides in the linked list of bucket `inode->dir->tb[n]`  where n is given by `hash_name(name)`.
diff --git a/benchmarks/specfs_bench/data/spec/inode/inode_find.spec b/benchmarks/specfs_bench/data/spec/inode/inode_find.spec
new file mode 100644
index 00000000..ddce59d3
--- /dev/null
+++ b/benchmarks/specfs_bench/data/spec/inode/inode_find.spec
@@ -0,0 +1,48 @@
+[PROMPT]
+Provide complete `inode_find.c` file that implement `inode_find` operation. You can use information from [RELY], [GUARANTEE] and [SPECIFICATION] as described below. Only provide the implementation of that single function and only include `inode.h` as the header. Your output is wrapped in a C code block, and no other unrelavent code should be given.
+
+[RELY]
+```c
+unsigned int hash_name(char* name);
+```
+```c
+typedef struct entry {
+	char *name;
+	void *inum;
+	struct entry *next;
+} entry;
+```
+```c
+typedef struct dirtb {
+	struct entry *tb[DIRTB_NUM];
+} dirtb;
+```
+```c
+typedef struct inode {
+	int mutex;
+	struct mcs_mutex *impl;
+	struct mcs_node *hd;
+	unsigned maj;
+	unsigned min;
+	unsigned int mode;
+	unsigned int size;
+	struct dirtb *dir;
+	struct indextb *file;
+} inode;
+```
+
+[GUARANTEE]
+```c
+struct inode *inode_find(struct inode *node, char *name);
+```
+
+[SPECIFICATION]
+**Pre-Condition**:
+there exists an inode pointed to by `node`. The inode is an directory, i.e., `node->dir` is not NULL.
+**Post-Condition**:
+there are two cases depending on whether the entry named `name` exists.
+Case1: if an entry named `name` exists in `cur`, the `inum` field of the entry is returned. 
+Case2: if an entry named `name` is not found in `cur`, the return value is NULL.
+
+**Invariant**: 
+**Directory well-formedness**: (1) Each child entry's name is different from others in the same directory. (2) In an inode `inode`, for each name `name`, its entry resides in the linked list of bucket `inode->dir->tb[n]`  where n is given by `hash_name(name)`.
diff --git a/benchmarks/specfs_bench/data/spec/inode/inode_insert.spec b/benchmarks/specfs_bench/data/spec/inode/inode_insert.spec
new file mode 100644
index 00000000..212b15fe
--- /dev/null
+++ b/benchmarks/specfs_bench/data/spec/inode/inode_insert.spec
@@ -0,0 +1,51 @@
+[PROMPT]
+Provide complete `inode_insert.c` file that implement `inode_insert` operation. You can use information from [RELY], [GUARANTEE] and [SPECIFICATION] as described below. Only provide the implementation of that single function and only include `inode.h` as the header. Your output is wrapped in a C code block, and no other unrelavent code should be given.
+
+[RELY]
+```c
+char* malloc_string(const char* name);
+```
+```c
+unsigned int hash_name(char* name);
+```
+```c
+typedef struct inode {
+	int mutex;
+	struct mcs_mutex *impl;
+	struct mcs_node *hd;
+	unsigned maj;
+	unsigned min;
+	unsigned int mode;
+	unsigned int size;
+	struct dirtb *dir;
+	struct indextb *file;
+} inode;
+```
+```c
+typedef struct dirtb {
+	struct entry *tb[DIRTB_NUM];
+} dirtb;
+```
+```c
+typedef struct entry {
+	char *name;
+	void *inum;
+	struct entry *next;
+} entry;
+```
+```c
+struct entry *malloc_entry();
+```
+
+[GUARANTEE]
+```c
+int inode_insert(struct inode* cur, struct inode* inum, char* name);
+```
+
+[SPECIFICATION]
+**Pre-Condition**:
+there exists an inode pointed to by `cur`. The `dir` field of `cur`records a fixed length array of heads of entry lists.
+**Post-Condition**:
+Case1: if the operation succeeds, a new `entry` is inserted into `cur` inode, whose fields are specified by the arguments of `inode_insert`. The new `entry` locates at the head of `cur->dir->tb[n]` where `n` is computed by `hash_name(name)`.  The size of `cur` increases by 1. The return value is 0.
+Case2: if the operation fails due to memory allocation failures, unused memory is freed and the return value is 1.
+
diff --git a/benchmarks/specfs_bench/data/spec/inode/inode_read.spec b/benchmarks/specfs_bench/data/spec/inode/inode_read.spec
new file mode 100644
index 00000000..285d017e
--- /dev/null
+++ b/benchmarks/specfs_bench/data/spec/inode/inode_read.spec
@@ -0,0 +1,56 @@
+[PROMPT]
+Provide complete `inode_read.c` file that implement `inode_read` operation. You can use information from [RELY], [GUARANTEE] and [SPECIFICATION] as described below. Only provide the implementation of that single function and only include `inode.h` as the header. Your output is wrapped in a C code block, and no other unrelavent code should be given.
+
+[RELY]
+```c
+void file_read(struct inode *node, unsigned offset, unsigned len, char *data);
+```
+```c
+struct read_ret* malloc_readret();
+```
+```c
+char* malloc_buffer(unsigned len);
+```
+```c
+typedef struct inode {
+	int mutex;
+	struct mcs_mutex *impl;
+	struct mcs_node *hd;
+	unsigned maj;
+	unsigned min;
+	unsigned int mode;
+	unsigned int size;
+	struct dirtb *dir;
+	struct indextb *file;
+} inode;
+```
+```c
+typedef struct read_ret {
+	char *buf;
+	unsigned num;
+} read_ret;
+```
+
+[GUARANTEE]
+```c
+struct read_ret* inode_read(struct inode* node, unsigned len, unsigned offset);
+```
+
+[SPECIFICATION]
+**Pre-Condition**:
+- `node` points to a valid inode structure with initialized `size` and `file` fields. the `file` field of the inode points to a valid `indextb` structure with `size` bytes allocated (non-NULL).
+**Post-Condition**:
+The function returns a non-NULL pointer to a dynamically allocated `read_ret` structure. Two cases define the outcome:
+
+**Case 1**: The read range is empty (`offset ≥ node->size` or `len == 0`).
+
+- `ret->num` = `0`.
+- `ret->buf` is  `NULL`
+
+**Case 2**: Data is read (`offset < node->size` and `len > 0`).
+
+- `ret->num` = `min(len, node->size - offset)` (actual bytes read).
+- `ret->buf` points to a buffer containing `ret->num` bytes copied from the file starting at `offset`.
+
+**System Algorithm**:
+*The caller is responsible for freeing `ret->buf` (if non-`NULL`) and the `read_ret` structure.*
diff --git a/benchmarks/specfs_bench/data/spec/inode/inode_truncate.spec b/benchmarks/specfs_bench/data/spec/inode/inode_truncate.spec
new file mode 100644
index 00000000..159bfa83
--- /dev/null
+++ b/benchmarks/specfs_bench/data/spec/inode/inode_truncate.spec
@@ -0,0 +1,38 @@
+[PROMPT]
+Provide complete `inode_truncate.c` file that implement `inode_truncate` operation. You can use information from [RELY], [GUARANTEE] and [SPECIFICATION] as described below. Only provide the implementation of that single function and only include `inode.h` as the header. Your output is wrapped in a C code block, and no other unrelavent code should be given.
+
+[RELY]
+```c
+void file_clear(struct inode *node, unsigned start, unsigned len);
+```
+```c
+void file_allocate(struct inode *node, unsigned offset, unsigned len);
+```
+```c
+typedef struct inode {
+	int mutex;
+	struct mcs_mutex *impl;
+	struct mcs_node *hd;
+	unsigned maj;
+	unsigned min;
+	unsigned int mode;
+	unsigned int size;
+	struct dirtb *dir;
+	struct indextb *file;
+} inode;
+```
+
+[GUARANTEE]
+```c
+void inode_truncate(struct inode* node, unsigned size);
+```
+
+[SPECIFICATION]
+**Pre-Condition**:
+- `node` points to a valid inode structure with initialized `size` and `file` fields. the `file` field of the inode points to a valid `indextb` structure with `size` bytes allocated (non-NULL).
+- `size` is a non-negative integer.
+**Post-Condition**:
+- Case 1: If `size` is less than the current size of the inode, the file is truncated to `size` bytes. The remaining bytes are cleared.
+- Case 2: If `size` is greater than or equal to the current size, allocate additional space in the file and clear the newly allocated space.
+
+
diff --git a/benchmarks/specfs_bench/data/spec/inode/inode_write.spec b/benchmarks/specfs_bench/data/spec/inode/inode_write.spec
new file mode 100644
index 00000000..70e88e10
--- /dev/null
+++ b/benchmarks/specfs_bench/data/spec/inode/inode_write.spec
@@ -0,0 +1,53 @@
+[PROMPT]
+Provide complete `inode_write.c` file that implement `inode_write` operation. You can use information from [RELY], [GUARANTEE] and [SPECIFICATION] as described below. Only provide the implementation of that single function and only include `inode.h` as the header. Your output is wrapped in a C code block, and no other unrelavent code should be given.
+
+[RELY]
+```c
+typedef struct inode {
+	int mutex;
+	struct mcs_mutex *impl;
+	struct mcs_node *hd;
+	unsigned maj;
+	unsigned min;
+	unsigned int mode;
+	unsigned int size;
+	struct dirtb *dir;
+	struct indextb *file;
+} inode;
+```
+```c
+#define PG_SIZE 4096
+#define INDEXTB_NUM 8192
+#define DIRTB_NUM 512
+#define MAX_FILE_LEN 256
+#define MAX_DIR_SIZE 10000000
+#define MAX_PATH_LEN 100
+#define MAX_FILE_SIZE ((unsigned)(INDEXTB_NUM * PG_SIZE))
+#define PAGE_SIZE (4096)
+```
+```c
+void file_allocate(struct inode *node, unsigned offset, unsigned len);
+```
+```c
+void file_clear(struct inode *node, unsigned start, unsigned len);
+```
+// `file_write` writes a given data buffer (or zeroes if `data` is `NULL`) into a file’s page-indexed storage, handling offsets, page boundaries, and partial writes until the specified length is covered.
+```c
+void file_write(struct inode *node, unsigned offset, unsigned len, const char *data);
+```
+
+[GUARANTEE]
+```c
+unsigned inode_write(struct inode* node, const char* buffer, unsigned len, unsigned offset);
+```
+
+[SPECIFICATION]
+**Pre-Condition**:
+- `node` points to a valid inode structure with initialized `size` and `file` fields. the `file` field of the inode points to a valid `indextb` structure with `size` bytes allocated (non-NULL).
+- `buffer` is a valid pointer to a buffer containing data to write.
+- `len` is a non-negative integer representing the number of bytes to write.
+- `offset` is a non-negative integer representing the position in the file to write the data.
+**Post-Condition**:
+- Calculate the new size of the file after the write operation. If the new size exceeds the maximum file size, truncate it to `MAX_FILE_SIZE`.
+- If the new size is greater than the current size, allocate additional space in the file, clear the newly allocated space, and set the node's size to the new size.
+- Write the data from `buffer` to the file at the specified `offset` and return the number of bytes written.
diff --git a/benchmarks/specfs_bench/data/spec/interface-util/check_del.spec b/benchmarks/specfs_bench/data/spec/interface-util/check_del.spec
new file mode 100644
index 00000000..da277674
--- /dev/null
+++ b/benchmarks/specfs_bench/data/spec/interface-util/check_del.spec
@@ -0,0 +1,77 @@
+[PROMPT]
+Provide complete `check_del.c` file that implement `check_del` operation. You can use information first from [RELY], [GUARANTEE] and [SPECIFICATION] in the first phase, then more information in the refine phase as described below. Only provide the implementation of that single function and only include `interface-util.h` as the header. Your output is wrapped in a C code block, and no other unrelavent code should be given.
+
+## First Prompt
+[RELY]
+```c
+typedef struct inode {
+	int mutex;
+	struct mcs_mutex *impl;
+	struct mcs_node *hd;
+	unsigned maj;
+	unsigned min;
+	unsigned int mode;
+	unsigned int size;
+	struct dirtb *dir;
+	struct indextb *file;
+} inode;
+```
+```c
+struct inode *inode_find(struct inode *node, char *name);
+```
+```c
+typedef struct dirtb {
+	struct entry *tb[DIRTB_NUM];
+} dirtb;
+```
+
+[GUARANTEE]
+```c
+int check_del(struct inode *cur, char *name);
+```
+
+[SPECIFICATION]
+**Pre-Condition**:
+  * `cur` is a pointer to a valid directory inode.
+  * `name` is a valid, non-NULL string representing the entry to be checked.
+**Post-Condition**:
+**Case 1 (Deletion is permissible)**:
+
+  * The entry `name` exists in `cur`(via `inode_find`).
+  * The entry is either a file or an empty directory (`mode != DIR_MODE` or `size == 0`).
+  * Returns `0`.
+
+**Case 2 (Deletion is not permissible)**:
+
+  * Returns `1` if any of the following are true:
+      * `cur` is `NULL`.
+      * The entry `name` does not exist within `cur`.
+      * The entry `name` is a directory that is not empty (`mode == DIR_MODE` and `size > 0`).
+
+
+
+## Refine Prompt
+[RELY]
+```c
+void lock(struct inode* inum);
+```
+```c
+void unlock(struct inode* inum);
+```
+
+[SPECIFICATION of check_del]
+**Pre-Condition**:
+The lock for the directory inode `cur` is held.
+**Post-Condition**:
+** If the function returns 0 (Success)**: The lock for `cur` AND the lock for the target inode (`inum`) are held.
+** If the function returns 1 (Failure)**: All locks(locks of `cur` and `inum`, if exist) are released. The caller owns no locks that were passed to or acquired in this function.
+
+
+
+[SPECIFICATION of inode_find]
+**Pre-Condition**:
+No lock assumptions.
+**Post-Condition**:
+No locks are acquired or released.
+
+
diff --git a/benchmarks/specfs_bench/data/spec/interface-util/check_dir.spec b/benchmarks/specfs_bench/data/spec/interface-util/check_dir.spec
new file mode 100644
index 00000000..51f4a9fd
--- /dev/null
+++ b/benchmarks/specfs_bench/data/spec/interface-util/check_dir.spec
@@ -0,0 +1,65 @@
+[PROMPT]
+Provide complete `check_dir.c` file that implement `check_dir` operation. You can use information first from [RELY], [GUARANTEE] and [SPECIFICATION] in the first phase, then more information in the refine phase as described below. Only provide the implementation of that single function and only include `interface-util.h` as the header. Your output is wrapped in a C code block, and no other unrelavent code should be given.
+
+## First Prompt
+[RELY]
+```c
+typedef struct inode {
+	int mutex;
+	struct mcs_mutex *impl;
+	struct mcs_node *hd;
+	unsigned maj;
+	unsigned min;
+	unsigned int mode;
+	unsigned int size;
+	struct dirtb *dir;
+	struct indextb *file;
+} inode;
+```
+```c
+#define FILE_MODE 1
+#define DIR_MODE 2
+#define CHR_MODE 3
+#define BLK_MODE 4
+#define SOCK_MODE 5
+#define FIFO_MODE 6
+```
+
+[GUARANTEE]
+```c
+int check_dir(struct inode *inum);
+```
+
+[SPECIFICATION]
+**Pre-Condition**:
+  * `inum`: A pointer to a `struct inode` that needs to be validated, or `NULL`.
+**Post-Condition**:
+**Case 1 (Success)**:
+
+  * The provided `inum` is not `NULL` and its `mode` field is equal to `DIR_MODE`.
+  * Returns `0` to indicate that it is a valid directory.
+
+**Case 2 (Failure)**:
+
+  * The provided `inum` is `NULL` or its `mode` field is not equal to `DIR_MODE`.
+  * Returns `1` to indicate that it is not a valid directory.
+
+
+**System Algorithm**:
+This function serves as a predicate to validate if a given inode handle represents a directory.
+
+## Refine Prompt
+[RELY]
+```c
+void unlock(struct inode* inum);
+```
+
+[SPECIFICATION of check_dir]
+**Pre-Condition**:
+  * If `inum` is not `NULL`, the lock for `inum` is owned by the current thread.
+**Post-Condition**:
+** If the function returns 0 (Success)**: The lock for `inum` remains owned by the current thread.
+** If the function returns 1 (Failure)**: No lock is owned by the current thread (specifically, if `inum` was not `NULL`, its lock has been released).
+
+
+
diff --git a/benchmarks/specfs_bench/data/spec/interface-util/check_file.spec b/benchmarks/specfs_bench/data/spec/interface-util/check_file.spec
new file mode 100644
index 00000000..804027cc
--- /dev/null
+++ b/benchmarks/specfs_bench/data/spec/interface-util/check_file.spec
@@ -0,0 +1,63 @@
+[PROMPT]
+Provide complete `check_file.c` file that implement `check_file` operation. You can use information first from [RELY], [GUARANTEE] and [SPECIFICATION] in the first phase, then more information in the refine phase as described below. Only provide the implementation of that single function and only include `interface-util.h` as the header. Your output is wrapped in a C code block, and no other unrelavent code should be given.
+
+## First Prompt
+[RELY]
+```c
+typedef struct inode {
+	int mutex;
+	struct mcs_mutex *impl;
+	struct mcs_node *hd;
+	unsigned maj;
+	unsigned min;
+	unsigned int mode;
+	unsigned int size;
+	struct dirtb *dir;
+	struct indextb *file;
+} inode;
+```
+```c
+#define FILE_MODE 1
+#define DIR_MODE 2
+#define CHR_MODE 3
+#define BLK_MODE 4
+#define SOCK_MODE 5
+#define FIFO_MODE 6
+```
+
+[GUARANTEE]
+```c
+int check_file(struct inode *inum);
+```
+
+[SPECIFICATION]
+**Pre-Condition**:
+  * `inum`: A pointer to an `inode` structure that needs to be validated. The function must handle cases where `inum` is `NULL`.
+**Post-Condition**:
+**Case 1 (Success - Is a file)**:
+  * The provided `inum` is not `NULL` and its `mode` is **not** `DIR_MODE`.
+  * Returns `0`.
+
+**Case 2 (Failure - Is not a file)**:
+  * The provided `inum` is `NULL` **or** its `mode` is `DIR_MODE`.
+  * Returns `1`.
+
+
+**System Algorithm**:
+The primary goal of this function is to verify if a given inode represents a regular file, not a directory.
+
+## Refine Prompt
+[RELY]
+```c
+void unlock(struct inode* inum);
+```
+
+[SPECIFICATION of check_file]
+**Pre-Condition**:
+  * If `inum` is not `NULL`, the lock for `inum` **must be held** by the caller.
+**Post-Condition**:
+  * If the function returns `0` (Success - Is a file), the lock for `inum` **is still held**.
+  * If the function returns `1` because `inum` is a directory, the lock for `inum` **is released**.
+  * If the function returns `1` because `inum` is `NULL`, no lock operation occurs.
+
+
diff --git a/benchmarks/specfs_bench/data/spec/interface-util/check_ins.spec b/benchmarks/specfs_bench/data/spec/interface-util/check_ins.spec
new file mode 100644
index 00000000..08da11ac
--- /dev/null
+++ b/benchmarks/specfs_bench/data/spec/interface-util/check_ins.spec
@@ -0,0 +1,72 @@
+[PROMPT]
+Provide complete `check_ins.c` file that implement `check_ins` operation. You can use information first from [RELY], [GUARANTEE] and [SPECIFICATION] in the first phase, then more information in the refine phase as described below. Only provide the implementation of that single function and only include `interface-util.h` as the header. Your output is wrapped in a C code block, and no other unrelavent code should be given.
+
+## First Prompt
+[RELY]
+```c
+struct inode *inode_find(struct inode *node, char *name);
+```
+```c
+typedef struct inode {
+	int mutex;
+	struct mcs_mutex *impl;
+	struct mcs_node *hd;
+	unsigned maj;
+	unsigned min;
+	unsigned int mode;
+	unsigned int size;
+	struct dirtb *dir;
+	struct indextb *file;
+} inode;
+```
+```c
+typedef struct dirtb {
+	struct entry *tb[DIRTB_NUM];
+} dirtb;
+```
+
+[GUARANTEE]
+```c
+int check_ins(struct inode *cur, char *name);
+```
+
+[SPECIFICATION]
+**Pre-Condition**:
+  * `cur`: A pointer to the target directory inode where the insertion is proposed.
+  * `name`: A valid, non-NULL string for the new entry's name.
+**Post-Condition**:
+**Case 1 (Success - Insertion is possible)**:
+  * Returns `0` if all the following conditions are met:
+      * `cur` is a valid directory (`cur->mode == DIR_MODE`).
+      * The directory `cur` is not full (`cur->size < MAX_DIR_SIZE`).
+      * An entry with `name` does not already exist in `cur`'s directory (check via `inode_find`).
+  * The state of `cur` and its contents remains unchanged.
+
+**Case 2 (Failure - Insertion is not possible)**:
+  * Returns `1` if any of the following conditions are true:
+      * `cur` is `NULL`.
+      * `cur` is not a directory (`cur->mode != DIR_MODE`).
+      * The directory `cur` is already full (`cur->size >= MAX_DIR_SIZE`).
+      * An entry with the given `name` already exists in `cur`.
+
+
+**System Algorithm**:
+To validate whether a new directory entry can be created within a parent directory inode `cur`.
+
+## Refine Prompt
+[RELY]
+```c
+void lock(struct inode* inum);
+```
+```c
+void unlock(struct inode* inum);
+```
+
+[SPECIFICATION of check_ins]
+**Pre-Condition**:
+The lock for the inode `cur` is held by the calling thread.
+**Post-Condition**:
+  * If the function returns `0` (Success), the lock for `cur` remains held.
+  * If the function returns `1` (Failure), the lock for `cur` is released before returning.
+
+
diff --git a/benchmarks/specfs_bench/data/spec/interface-util/check_open.spec b/benchmarks/specfs_bench/data/spec/interface-util/check_open.spec
new file mode 100644
index 00000000..ccd40de8
--- /dev/null
+++ b/benchmarks/specfs_bench/data/spec/interface-util/check_open.spec
@@ -0,0 +1,70 @@
+[PROMPT]
+Provide complete `check_open.c` file that implement `check_open` operation. You can use information first from [RELY], [GUARANTEE] and [SPECIFICATION] in the first phase, then more information in the refine phase as described below. Only provide the implementation of that single function and only include `interface-util.h` as the header. Your output is wrapped in a C code block, and no other unrelavent code should be given.
+
+## First Prompt
+[RELY]
+```c
+typedef struct inode {
+	int mutex;
+	struct mcs_mutex *impl;
+	struct mcs_node *hd;
+	unsigned maj;
+	unsigned min;
+	unsigned int mode;
+	unsigned int size;
+	struct dirtb *dir;
+	struct indextb *file;
+} inode;
+```
+```c
+#define FILE_MODE 1
+#define DIR_MODE 2
+#define CHR_MODE 3
+#define BLK_MODE 4
+#define SOCK_MODE 5
+#define FIFO_MODE 6
+```
+
+[GUARANTEE]
+```c
+int check_open(struct inode *inum, unsigned mode);
+```
+
+[SPECIFICATION]
+**Pre-Condition**:
+  * `inum`: A pointer to an inode structure, which can be NULL.
+  * `mode`: The file mode to be checked for compatibility.
+**Post-Condition**:
+**Case 1 (Success - Compatible modes)**:
+
+  * Returns `0` if `inum` is not NULL and its mode is compatible with the provided `mode`. Compatibility is defined as:
+      * `inum->mode` is `DIR_MODE` and `mode` is `DIR_MODE`.
+      * `inum->mode` is not `DIR_MODE` and `mode` is not `DIR_MODE`.
+
+**Case 2 (Failure - Incompatible modes or NULL inode)**:
+
+  * Returns `1` if any of the following conditions are met:
+      * a) `inum` is NULL.
+      * b) `inum->mode` is `DIR_MODE`, but the provided `mode` is not.
+      * c) `inum->mode` is not `DIR_MODE`, but the provided `mode` is.
+
+
+**Invariant**: 
+**Well-formedness of inode**: If `inum` is not NULL, it must point to a valid, initialized inode.
+
+## Refine Prompt
+[RELY]
+```c
+void lock(struct inode* inum);
+```
+```c
+void unlock(struct inode* inum);
+```
+
+[SPECIFICATION of check_open]
+**Pre-Condition**:
+If `inum` is not NULL, the lock for `inum` is owned.
+**Post-Condition**:
+No lock is owned.
+
+
diff --git a/benchmarks/specfs_bench/data/spec/interface-util/check_src_exist_dst_delete.spec b/benchmarks/specfs_bench/data/spec/interface-util/check_src_exist_dst_delete.spec
new file mode 100644
index 00000000..2c324238
--- /dev/null
+++ b/benchmarks/specfs_bench/data/spec/interface-util/check_src_exist_dst_delete.spec
@@ -0,0 +1,110 @@
+[PROMPT]
+Provide complete `check_src_exist_dst_delete.c` file that implement `check_src_exist_dst_delete` operation. You can use information first from [RELY], [GUARANTEE] and [SPECIFICATION] in the first phase, then more information in the refine phase as described below. Only provide the implementation of that single function and only include `interface-util.h` as the header. Your output is wrapped in a C code block, and no other unrelavent code should be given.
+
+## First Prompt
+[RELY]
+```c
+typedef struct inode {
+	int mutex;
+	struct mcs_mutex *impl;
+	struct mcs_node *hd;
+	unsigned maj;
+	unsigned min;
+	unsigned int mode;
+	unsigned int size;
+	struct dirtb *dir;
+	struct indextb *file;
+} inode;
+```
+```c
+typedef struct dirtb {
+	struct entry *tb[DIRTB_NUM];
+} dirtb;
+```
+```c
+struct inode *inode_find(struct inode *node, char *name);
+```
+```c
+#define FILE_MODE 1
+#define DIR_MODE 2
+#define CHR_MODE 3
+#define BLK_MODE 4
+#define SOCK_MODE 5
+#define FIFO_MODE 6
+```
+```c
+#define PG_SIZE 4096
+#define INDEXTB_NUM 8192
+#define DIRTB_NUM 512
+#define MAX_FILE_LEN 256
+#define MAX_DIR_SIZE 10000000
+#define MAX_PATH_LEN 100
+#define MAX_FILE_SIZE ((unsigned)(INDEXTB_NUM * PG_SIZE))
+#define PAGE_SIZE (4096)
+```
+
+[GUARANTEE]
+```c
+int check_src_exist_dst_delete(struct inode *srcdir, struct inode *dstdir, char *srcname, char *dstname);
+```
+
+[SPECIFICATION]
+**Pre-Condition**:
+  - `srcdir`, `dstdir`: Non-NULL pointers to valid `inode` structures.
+  - `srcname`, `dstname`: Non-NULL, NULL-terminated strings representing entry names.
+**Post-Condition**:
+The function checks several conditions for a rename-like operation and returns an integer status.
+
+**Case 1 (Success)**: If all of the following conditions (1)-(3) are met, the function returns **0**.
+
+1.  **Source Existence**: An inode named `srcname` exists under `srcdir`. Let this be `srcinode`.
+2.  **Destination Directory Validity**:
+      - `dstdir` must be a directory (i.e., `dstdir->mode == DIR_MODE`).
+      - `dstdir` must have space for a new entry (i.e., `dstdir->size < MAX_DIR_SIZE`).
+3.  **Destination Entry Validity**: If an inode named `dstname` exists under `dstdir` (let it be `dstinode`), then all of the following must be true:
+      - If `srcinode` is the same as `dstinode`, the validity is held.
+      - If `srcinode` is not the same as `dstinode`, then:
+        - `srcinode` and `dstinode` have compatible types (either both are directories or both are not directories).
+        - If `dstinode` is a directory, it must be empty (i.e., `dstinode->size == 0`).
+
+**Case 2 (Failure)**: If any condition in Case 1 is not met, the function returns **1**.
+
+
+**Invariant**: 
+**Valid Directories**: The input inodes `srcdir` and `dstdir` point to valid, initialized inode structures.
+
+## Refine Prompt
+[RELY]
+```c
+void lock(struct inode* inum);
+```
+```c
+void unlock(struct inode* inum);
+```
+// unlock the lock of srcdir and dstdir.
+```c
+void unlock2dir (struct inode* srcdir, struct inode* dstdir);
+```
+
+[SPECIFICATION of check_src_exist_dst_delete]
+**Pre-Condition**:
+  - The caller must hold the locks for both `srcdir` and `dstdir` before calling this function.
+**Post-Condition**:
+  - **On Failure (return 1)**: All locks held upon entry and acquired during execution are released. No locks are held by this function upon return.
+  - **On Success (return 0)**:
+      - The locks on `srcdir` and `dstdir` remain held.
+      - If `dstinode` existed, its lock also remains held.
+      - The lock on `srcinode` (if acquired) is released.
+
+**System Algorithm**:
+1.  Check for the existence of `srcinode` (the entry named `srcname` in `srcdir`).
+2.  Check the validity of `dstdir` (mode and size).
+3.  If an entry named `dstname` exists in `dstdir` (let it be `dstinode`):
+      - Acquire the lock for `srcinode`.
+      - Acquire the lock for `dstinode`.
+      - Perform checks on `srcinode` and `dstinode` (type compatibility, directory emptiness).
+      - After the checks are complete, release the lock on `srcinode`.
+      - **Important**: The lock on `dstinode` is **not** released if it exists and all checks pass. It is held for the subsequent deletion operation by the caller.
+4.  **Error Handling**: If any check fails at any point, release all locks currently held (`srcdir`, `dstdir`, and if acquired, `srcinode` and `dstinode`) and return.
+
+
diff --git a/benchmarks/specfs_bench/data/spec/interface-util/check_unlock.spec b/benchmarks/specfs_bench/data/spec/interface-util/check_unlock.spec
new file mode 100644
index 00000000..06fde949
--- /dev/null
+++ b/benchmarks/specfs_bench/data/spec/interface-util/check_unlock.spec
@@ -0,0 +1,25 @@
+[PROMPT]
+Provide complete `check_unlock.c` file that implement `check_unlock` operation. You can use information from [RELY], [GUARANTEE] and [SPECIFICATION] as described below. Only provide the implementation of that single function and only include `interface-util.h` as the header. Your output is wrapped in a C code block, and no other unrelavent code should be given.
+
+[RELY]
+```c
+void unlock(struct inode* inum);
+```
+
+[GUARANTEE]
+```c
+void check_unlock (struct inode* parent, struct inode* src, struct inode* dst);
+```
+
+[SPECIFICATION]
+**Pre-Condition**:
+- `parent`, `src`, and `dst` are non-NULL inode pointers
+- `parent`  is currently locked
+**Post-Condition**:
+The function conditionally unlocks `parent` based on pointer comparison:
+
+- **Case 1 (Unlock performed)**:
+  If `parent` distinct from both `src` and `dst`, `parent` is unlocked.
+- **Case 2 (No unlock)**:
+  If  `parent == src` OR `parent == dst`, no operation occurs.
+
diff --git a/benchmarks/specfs_bench/data/spec/interface/atomfs_del.spec b/benchmarks/specfs_bench/data/spec/interface/atomfs_del.spec
new file mode 100644
index 00000000..e11a4ca2
--- /dev/null
+++ b/benchmarks/specfs_bench/data/spec/interface/atomfs_del.spec
@@ -0,0 +1,90 @@
+[PROMPT]
+Provide complete `atomfs_del.c` file that implement `atomfs_del` operation. You can use information first from [RELY], [GUARANTEE] and [SPECIFICATION] in the first phase, then more information in the refine phase as described below. Only provide the implementation of that single function and only include `interface.h` as the header. Your output is wrapped in a C code block, and no other unrelavent code should be given.
+
+## First Prompt
+[RELY]
+```c
+typedef struct inode {
+	int mutex;
+	struct mcs_mutex *impl;
+	struct mcs_node *hd;
+	unsigned maj;
+	unsigned min;
+	unsigned int mode;
+	unsigned int size;
+	struct dirtb *dir;
+	struct indextb *file;
+} inode;
+```
+```c
+extern struct inode *root_inum;
+```
+// Traverse path under cur. If an inode is found, the return value is the found inode. If no inode is found, the return value is NULL. The lock of cur is released before returning, and the lock of the found inode is acquired.
+```c
+struct inode* locate(struct inode* cur, char* path[]);
+```
+// Check if the inode with the given name can be deleted under the current inode. Returns 0 if deletion is allowed, 1 otherwise while releasing the lock.
+```c
+int check_del(struct inode *cur, char *name);
+```
+// Delete the inode with the given name under inum. Returns the deleted inode if successful, NULL otherwise.
+```c
+struct inode* inode_delete(struct inode* inum, char* name);
+```
+// Dispose of the inode, releasing all associated resources.
+```c
+void dispose_inode(struct inode* inum);
+```
+
+[GUARANTEE]
+```c
+int atomfs_del(char* path[], char* name);
+```
+
+[SPECIFICATION]
+**Pre-Condition**:
+- `path`: A NULL-terminated string array representing the path to the parent directory.
+- `name`: A valid, non-null string representing the name of the file or directory to be deleted.
+**Post-Condition**:
+Case 1 (Successful Deletion):
+- The directory entry corresponding to `name` is removed from the target directory found at `path`.
+- The inode previously associated with `name` is deallocated.
+- Returns 0.
+
+Case 2 (Failure):
+- The file system state remains unchanged.
+- Returns `-1` if the path traversal fails (starting from `root_inum`, by following the `path` via `locate`, it returns `NULL`) or the deletion check fails (check_del returns a non-zero value).
+
+**Invariant**: 
+Root Existence: The global `root_inum` must always point to a valid, initialized directory inode.
+
+## Refine Prompt
+[RELY]
+```c
+void lock(struct inode* inum);
+```
+```c
+void unlock(struct inode* inum);
+```
+
+[SPECIFICATION of locate]
+**Pre-Condition**:
+The `cur` inode must be locked.
+**Post-Condition**:
+If a target inode is returned, it is locked, and all intermediate locks (including the initial lock on `cur`) have been released. If `NULL` is returned, all locks have been released.
+
+
+[SPECIFICATION of check_del]
+**Pre-Condition**:
+The `cur` inode must be locked.
+**Post-Condition**:
+If the function returns 0 (success), the lock on `cur` is still held. If it returns non-zero (failure), the lock on `cur` is released.
+
+
+[SPECIFICATION of atomfs_del]
+**Pre-Condition**:
+No lock is owned.
+**Post-Condition**:
+No lock is owned.
+
+
diff --git a/benchmarks/specfs_bench/data/spec/interface/atomfs_getattr.spec b/benchmarks/specfs_bench/data/spec/interface/atomfs_getattr.spec
new file mode 100644
index 00000000..7b648c81
--- /dev/null
+++ b/benchmarks/specfs_bench/data/spec/interface/atomfs_getattr.spec
@@ -0,0 +1,81 @@
+[PROMPT]
+Provide complete `atomfs_getattr.c` file that implement `atomfs_getattr` operation. You can use information first from [RELY], [GUARANTEE] and [SPECIFICATION] in the first phase, then more information in the refine phase as described below. Only provide the implementation of that single function and only include `interface.h` as the header. Your output is wrapped in a C code block, and no other unrelavent code should be given.
+
+## First Prompt
+[RELY]
+// Traverse path under cur. If an inode is found, the return value is the found inode. If no inode is found, the return value is NULL. The lock of cur is released before returning, and the lock of the found inode is acquired.
+```c
+struct inode* locate(struct inode* cur, char* path[]);
+```
+```c
+struct getattr_ret* malloc_getattr_ret(struct inode* inum, unsigned mode, unsigned size, unsigned maj, unsigned min);
+```
+```c
+typedef struct getattr_ret {
+	struct inode *inum;
+	unsigned mode;
+	unsigned size;
+	unsigned maj;
+	unsigned min;
+} getattr_ret;
+```
+```c
+typedef struct inode {
+	int mutex;
+	struct mcs_mutex *impl;
+	struct mcs_node *hd;
+	unsigned maj;
+	unsigned min;
+	unsigned int mode;
+	unsigned int size;
+	struct dirtb *dir;
+	struct indextb *file;
+} inode;
+```
+
+[GUARANTEE]
+```c
+struct getattr_ret* atomfs_getattr(char* path[]);
+```
+
+[SPECIFICATION]
+**Pre-Condition**:
+  * `path` must be a valid NULL-terminated array of strings representing the path to the target inode.
+**Post-Condition**:
+**Case 1 (Successful lookup)**:
+
+  * Starting from `root_inum`, the path is successfully traversed to find the target inode.
+  * A new `getattr_ret` structure is allocated and populated with the attributes (`mode`, `size`, `maj`, `min`) of the found inode.
+  * Returns a pointer to the newly allocated `getattr_ret` structure.
+
+**Case 2 (Lookup failure)**:
+
+  * Returns `NULL` if the path traversal fails (`locate` returns NULL).
+
+**Invariant**: 
+**Well-formedness of root_inum**: The global `root_inum` must point to a valid, initialized directory inode.
+
+## Refine Prompt
+[RELY]
+```c
+void lock(struct inode* inum);
+```
+```c
+void unlock(struct inode* inum);
+```
+
+[SPECIFICATION of locate]
+**Pre-Condition**:
+`cur` is locked.
+**Post-Condition**:
+If `target` is NULL, `locate` would have released all locks, so no lock is owned in this case.
+If `target` is not NULL, only the lock of `target` is owned. `locate` would have released all other locks.
+
+
+[SPECIFICATION of atomfs_getattr]
+**Pre-Condition**:
+no lock is owned.
+**Post-Condition**:
+no lock is owned.
+
+
diff --git a/benchmarks/specfs_bench/data/spec/interface/atomfs_ins.spec b/benchmarks/specfs_bench/data/spec/interface/atomfs_ins.spec
new file mode 100644
index 00000000..231755a1
--- /dev/null
+++ b/benchmarks/specfs_bench/data/spec/interface/atomfs_ins.spec
@@ -0,0 +1,95 @@
+[PROMPT]
+Provide complete `atomfs_ins.c` file that implement `atomfs_ins` operation. You can use information first from [RELY], [GUARANTEE] and [SPECIFICATION] in the first phase, then more information in the refine phase as described below. Only provide the implementation of that single function and only include `interface.h` as the header. Your output is wrapped in a C code block, and no other unrelavent code should be given.
+
+## First Prompt
+[RELY]
+```c
+typedef struct inode {
+	int mutex;
+	struct mcs_mutex *impl;
+	struct mcs_node *hd;
+	unsigned maj;
+	unsigned min;
+	unsigned int mode;
+	unsigned int size;
+	struct dirtb *dir;
+	struct indextb *file;
+} inode;
+```
+```c
+extern struct inode *root_inum;
+```
+// Traverse path under cur. If an inode is found, the return value is the found inode. If no inode is found, the return value is NULL. The lock of cur is released before returning, and the lock of the found inode is acquired.
+```c
+struct inode* locate(struct inode* cur, char* path[]);
+```
+// initialize a new inode. Its `mode`, `maj`, `min` fields are filled with the arguments. the return value is non-NULL.
+```c
+struct inode* malloc_inode(int mode, unsigned maj, unsigned min);
+```
+// Check whether name can be successfully inserted to cur. If the insertion can succeed, the return value is 0. If the insertion should fail, the return value is 1.
+```c
+int check_ins(struct inode *cur, char *name);
+```
+// a new entry is inserted to cur, whose fields are specified by inum and name.
+```c
+int inode_insert(struct inode* cur, struct inode* inum, char* name);
+```
+
+[GUARANTEE]
+```c
+int atomfs_ins(char* path[], char* name, int mode, unsigned maj, unsigned min);
+```
+
+[SPECIFICATION]
+**Pre-Condition**:
+- `name` must be a valid string (non-NULL) for the new entry.
+- `path` must be a valid NULL-terminated array of strings
+**Post-Condition**:
+**Case 1 (Successful traversal and insertion)**:
+
+- A new inode with specified `mode`, `maj`, and `min` is allocated.
+- The new entry `(name, inode)` is inserted into the target directory.
+- Returns `0` to indicate success.
+
+**Case 2 (Traversal or insertion failure)**:
+
+- Returns `-1` if either:
+  a) The path traversal fails (starting from `root_inum`, by following the path, `locate` returns NULL).
+  b) Insertion check fails (`check_ins` returns non-zero).
+
+**Invariant**: 
+**Well-formedness of root_inum**: The global `root_inum` must point to a valid, initialized directory inode.
+
+## Refine Prompt
+[RELY]
+```c
+void lock(struct inode* inum);
+```
+```c
+void unlock(struct inode* inum);
+```
+
+[SPECIFICATION of locate]
+**Pre-Condition**:
+cur is locked.
+**Post-Condition**:
+If target is NULL, locate would have released all locks, so no lock is owned in this case.
+If target is not NULL, only the lock of target is owned. locate would have released all other locks.
+
+
+[SPECIFICATION of check_ins]
+**Pre-Condition**:
+cur is locked.
+**Post-Condition**:
+if check_ins returns 0, cur is locked. 
+If check_ins returns 1, no lock is owned.
+
+
+[SPECIFICATION of atomfs_ins]
+**Pre-Condition**:
+no lock is owned. 
+**Post-Condition**:
+no lock is owned. 
+
+
diff --git a/benchmarks/specfs_bench/data/spec/interface/atomfs_open.spec b/benchmarks/specfs_bench/data/spec/interface/atomfs_open.spec
new file mode 100644
index 00000000..de8edad4
--- /dev/null
+++ b/benchmarks/specfs_bench/data/spec/interface/atomfs_open.spec
@@ -0,0 +1,85 @@
+[PROMPT]
+Provide complete `atomfs_open.c` file that implement `atomfs_open` operation. You can use information first from [RELY], [GUARANTEE] and [SPECIFICATION] in the first phase, then more information in the refine phase as described below. Only provide the implementation of that single function and only include `interface.h` as the header. Your output is wrapped in a C code block, and no other unrelavent code should be given.
+
+## First Prompt
+[RELY]
+```c
+typedef struct inode {
+	int mutex;
+	struct mcs_mutex *impl;
+	struct mcs_node *hd;
+	unsigned maj;
+	unsigned min;
+	unsigned int mode;
+	unsigned int size;
+	struct dirtb *dir;
+	struct indextb *file;
+} inode;
+```
+```c
+extern struct inode *root_inum;
+```
+// Traverse path under cur. If an inode is found, the return value is the found inode. If no inode is found, the return value is NULL. The lock of cur is released before returning, and the lock of the found inode is acquired.
+```c
+struct inode* locate(struct inode* cur, char* path[]);
+```
+```c
+int check_open(struct inode *inum, unsigned mode);
+```
+
+[GUARANTEE]
+```c
+struct inode *atomfs_open(char *path[], unsigned mode);
+```
+
+[SPECIFICATION]
+**Pre-Condition**:
+  * `path` must be a valid, NULL-terminated array of strings representing the file path.
+  * `mode` is an unsigned integer representing the desired access mode.
+**Post-Condition**:
+**Case 1 (Successful open)**:
+
+  * The path is successfully traversed to find the target inode.
+  * The open check for the given mode is successful.
+  * Returns a pointer to the target inode.
+
+**Case 2 (Failure to open)**:
+
+  * Returns `NULL` if either:
+      * a) The path traversal fails (starting from `root_inum`, by following the path, `locate` returns `NULL`).
+      * b) The open check fails (`check_open` returns a non-zero value).
+
+**Invariant**: 
+**Well-formedness of root_inum**: The global `root_inum` must always point to a valid, initialized directory inode.
+
+## Refine Prompt
+[RELY]
+```c
+void lock(struct inode* inum);
+```
+```c
+void unlock(struct inode* inum);
+```
+
+[SPECIFICATION of locate]
+**Pre-Condition**:
+`cur` is locked.
+**Post-Condition**:
+  * If `locate` returns a non-NULL `target`, only the lock on `target` is held. All other intermediate locks have been released.
+  * If `locate` returns `NULL`, no locks are held.
+
+
+[SPECIFICATION of check_open]
+**Pre-Condition**:
+`inum` is locked.
+**Post-Condition**:
+`inum` is unlocked.
+
+
+[SPECIFICATION of atomfs_open]
+**Pre-Condition**:
+No locks are held.
+**Post-Condition**:
+No locks are held.
+
+
diff --git a/benchmarks/specfs_bench/data/spec/interface/atomfs_read.spec b/benchmarks/specfs_bench/data/spec/interface/atomfs_read.spec
new file mode 100644
index 00000000..ca093e82
--- /dev/null
+++ b/benchmarks/specfs_bench/data/spec/interface/atomfs_read.spec
@@ -0,0 +1,89 @@
+[PROMPT]
+Provide complete `atomfs_read.c` file that implement `atomfs_read` operation. You can use information first from [RELY], [GUARANTEE] and [SPECIFICATION] in the first phase, then more information in the refine phase as described below. Only provide the implementation of that single function and only include `interface.h` as the header. Your output is wrapped in a C code block, and no other unrelavent code should be given.
+
+## First Prompt
+[RELY]
+```c
+typedef struct inode {
+	int mutex;
+	struct mcs_mutex *impl;
+	struct mcs_node *hd;
+	unsigned maj;
+	unsigned min;
+	unsigned int mode;
+	unsigned int size;
+	struct dirtb *dir;
+	struct indextb *file;
+} inode;
+```
+```c
+extern struct inode *root_inum;
+```
+```c
+typedef struct read_ret {
+	char *buf;
+	unsigned num;
+} read_ret;
+```
+// Traverse path under cur. If an inode is found, the return value is the found inode. If no inode is found, the return value is NULL. The lock of cur is released before returning, and the lock of the found inode is acquired.
+```c
+struct inode* locate(struct inode* cur, char* path[]);
+```
+```c
+int check_file(struct inode *inum);
+```
+```c
+struct read_ret* inode_read(struct inode* node, unsigned len, unsigned offset);
+```
+
+[GUARANTEE]
+```c
+struct read_ret* atomfs_read(char* path[], unsigned size, unsigned offset);
+```
+
+[SPECIFICATION]
+**Pre-Condition**:
+`root_inum` is a valid directory inode. The `path` corresponds to an existing entry in the file system hierarchy rooted at `root_inum`, ensuring `locate(root_inum, path)` returns a valid non-NULL inode.
+**Post-Condition**:
+The return value depends on the validity of the located inode and the read operation:
+
+**Case 1**: Starting from `root_inum`, by following the `path`, find the `inum`. If `check_file(inum)` indicates the inode is not readable (returns `1`), the function returns `NULL`.
+
+**Case 2**: Otherwise, the function reads `size` bytes from `buf` at `offset` into the file via `inode_read` and returns the result of `inode_read`. 
+
+
+
+## Refine Prompt
+[RELY]
+```c
+void lock(struct inode* inum);
+```
+```c
+void unlock(struct inode* inum);
+```
+
+[SPECIFICATION of locate]
+**Pre-Condition**:
+cur is locked.
+**Post-Condition**:
+If target is NULL, locate would have released all locks, so no lock is owned in this case.
+If target is not NULL, only the lock of target is owned. locate would have released all other locks.
+
+
+[SPECIFICATION of atomfs_read]
+**Pre-Condition**:
+no lock is owned. You should first acquire the lock of root_inum.
+**Post-Condition**:
+no lock is owned.
+
+
+[SPECIFICATION of check_file]
+**Pre-Condition**:
+If `inum` is not NULL, it is locked.
+**Post-Condition**:
+Failure, return 1:
+`inum` is NULL or `1num` is a directory, the lock is released and returned.
+Success, return 0:
+`inum` is still locked.
+
+
diff --git a/benchmarks/specfs_bench/data/spec/interface/atomfs_readdir.spec b/benchmarks/specfs_bench/data/spec/interface/atomfs_readdir.spec
new file mode 100644
index 00000000..cfaddeb6
--- /dev/null
+++ b/benchmarks/specfs_bench/data/spec/interface/atomfs_readdir.spec
@@ -0,0 +1,97 @@
+[PROMPT]
+Provide complete `atomfs_readdir.c` file that implement `atomfs_readdir` operation. You can use information first from [RELY], [GUARANTEE] and [SPECIFICATION] in the first phase, then more information in the refine phase as described below. Only provide the implementation of that single function and only include `interface.h` as the header. Your output is wrapped in a C code block, and no other unrelavent code should be given.
+
+## First Prompt
+[RELY]
+```c
+typedef struct inode {
+	int mutex;
+	struct mcs_mutex *impl;
+	struct mcs_node *hd;
+	unsigned maj;
+	unsigned min;
+	unsigned int mode;
+	unsigned int size;
+	struct dirtb *dir;
+	struct indextb *file;
+} inode;
+```
+```c
+extern struct inode *root_inum;
+```
+// Traverse path under cur. If an inode is found, the return value is the found inode. If no inode is found, the return value is NULL. The lock of cur is released before returning, and the lock of the found inode is acquired.
+```c
+struct inode* locate(struct inode* cur, char* path[]);
+```
+```c
+int check_dir(struct inode *inum);
+```
+```c
+char** malloc_dir_content(unsigned size);
+```
+```c
+void fill_dir(struct inode* inum, char** dircontent);
+```
+```c
+typedef struct dirtb {
+	struct entry *tb[DIRTB_NUM];
+} dirtb;
+```
+
+[GUARANTEE]
+```c
+char **atomfs_readdir(char *path[]);
+```
+
+[SPECIFICATION]
+**Pre-Condition**:
+  * `path` must be a valid NULL-terminated array of strings representing the path to the directory.
+**Post-Condition**:
+**Case 1 (Successful read)**:
+
+  * Starting from `root_inum`, the path successfully resolves to a valid directory inode.
+  * An array of strings of size `target->size + 1`(should plus 1 for NULL-terminated property), with the last element being NULL, is allocated and returned, containing the names of the entries in that directory.
+
+**Case 2 (Failure)**:
+
+  * Returns `NULL` if either:
+    a) The path traversal fails (`locate` returns NULL).
+    b) The target inode is not a directory (`check_dir` returns a non-zero value).
+
+
+**Invariant**: 
+**Well-formedness of root_inum**: The global `root_inum` must point to a valid, initialized directory inode.
+
+## Refine Prompt
+[RELY]
+```c
+void lock(struct inode* inum);
+```
+```c
+void unlock(struct inode* inum);
+```
+
+[SPECIFICATION of locate]
+**Pre-Condition**:
+`cur` is locked.
+**Post-Condition**:
+If `target` is `NULL`, all locks acquired during traversal have been released.
+If `target` is not `NULL`, only the lock for `target` is held. All other intermediate locks have been released.
+
+
+
+[SPECIFICATION of check_dir]
+**Pre-Condition**:
+`inum` is locked.
+**Post-Condition**:
+If `check_dir` returns 0 (success), the lock on `inum` is still held.
+If `check_dir` returns 1 (failure), the lock on `inum` has been released.
+
+
+[SPECIFICATION of atomfs_readdir]
+**Pre-Condition**:
+No lock is held.
+**Post-Condition**:
+No lock is held.
+
+
diff --git a/benchmarks/specfs_bench/data/spec/interface/atomfs_rename.spec b/benchmarks/specfs_bench/data/spec/interface/atomfs_rename.spec
new file mode 100644
index 00000000..7cdd4f40
--- /dev/null
+++ b/benchmarks/specfs_bench/data/spec/interface/atomfs_rename.spec
@@ -0,0 +1,196 @@
+[PROMPT]
+Provide complete `atomfs_rename.c` file that implement `atomfs_rename` operation. You can use information first from [RELY], [GUARANTEE] and [SPECIFICATION] in the first phase, then more information in the refine phase as described below. Only provide the implementation of that single function and only include `interface.h` as the header. Your output is wrapped in a C code block, and no other unrelavent code should be given.
+
+## First Prompt
+[RELY]
+```c
+typedef struct inode {
+	int mutex;
+	struct mcs_mutex *impl;
+	struct mcs_node *hd;
+	unsigned maj;
+	unsigned min;
+	unsigned int mode;
+	unsigned int size;
+	struct dirtb *dir;
+	struct indextb *file;
+} inode;
+```
+```c
+extern struct inode *root_inum;
+```
+// Delete the inode with the given name under inum. Returns the deleted inode if successful, NULL otherwise.
+```c
+struct inode* inode_delete(struct inode* inum, char* name);
+```
+// a new entry is inserted to cur, whose fields are specified by inum and name.
+```c
+int inode_insert(struct inode* cur, struct inode* inum, char* name);
+```
+```c
+struct inode *inode_find(struct inode *node, char *name);
+```
+// Dispose of the inode, releasing all associated resources.
+```c
+void dispose_inode(struct inode* inum);
+```
+```c
+int check_src_exist_dst_delete(struct inode *srcdir, struct inode *dstdir, char *srcname, char *dstname);
+```
+// malloc and return the common part of srcpath and dstpath
+```c
+char** calculate(char* srcpath[], char* dstpath[]);
+```
+```c
+void free_path(char** path);
+```
+```c
+int getlen(char* path[]);
+```
+```c
+struct inode* locate_hold(struct inode *cur, char *path[]);
+```
+// Traverse path under cur. If an inode is found, the return value is the found inode. If no inode is found, the return value is NULL. The lock of cur is released before returning, and the lock of the found inode is acquired.
+```c
+struct inode* locate(struct inode* cur, char* path[]);
+```
+// unlock parent if it is not equal to src and dst
+```c
+void check_unlock (struct inode* parent, struct inode* src, struct inode* dst);
+```
+
+[GUARANTEE]
+```c
+int atomfs_rename(char* srcpath[], char* dstpath[], char* srcname, char* dstname);
+```
+
+[SPECIFICATION]
+**Pre-Condition**:
+  * `srcpath`, `dstpath`, `srcname`, and `dstname` are valid, non-NULL pointers.
+**Post-Condition**:
+There are two possible outcomes:
+
+**Case 1 (Success)**: If all of the following conditions (1-3) are met:
+
+1.  **Parent Directories Valid**:
+      * Traversing `srcpath` from `root_inum` successfully finds a directory inode `srcdir`.
+      * Traversing `dstpath` from `root_inum` successfully finds a directory inode `dstdir`.
+2.  Source exists and destination is compatible.
+
+Then the following state changes occur:
+
+  * The entry for `srcname` is removed from `srcdir`.
+  * If `dstinode` existed, it is removed from `dstdir` and its resources are disposed of.
+  * A new entry for `srcinode` is created in `dstdir` with the name `dstname`.
+  * The function returns **0**.
+
+**Case 2 (Failure)**: If any of the conditions in Case 1 are not met, the file system state remains unchanged, and the function returns **-1**.
+
+
+**Invariant**: 
+**Well-formedness of root_inum**: The global `root_inum` must point to a valid, initialized directory inode.
+**System Algorithm**:
+The operation is implemented by first traversing to the source and destination parent directories, performing a series of validation checks, and then executing the move. The high-level logic is:
+
+1.  Calculate the common path between `srcpath` and `dstpath`.
+2.  Traverse from the root to the common ancestor directory (`parent`).
+3.  From `parent`, traverse the remaining paths to find the source directory (`srcdir`) and destination directory (`dstdir`).
+4.  Perform checks for existence, type compatibility, and other constraints on the source (`srcname`) and destination (`dstname`).
+5.  If all checks pass, atomically perform the rename.
+6.  Clean up any resources (e.g., the old destination inode if it was overwritten).
+
+
+## Refine Prompt
+[RELY]
+```c
+void lock(struct inode* inum);
+```
+```c
+void unlock(struct inode* inum);
+```
+// Traverse path under cur. If an inode is found, the return value is the found inode. If no inode is found, the return value is NULL. The lock of cur is released before returning, and the lock of the found inode is acquired.
+```c
+struct inode* locate(struct inode* cur, char* path[]);
+```
+```c
+struct inode* locate_hold(struct inode *cur, char *path[]);
+```
+// unlock parent if it is not equal to src and dst
+```c
+void check_unlock (struct inode* parent, struct inode* src, struct inode* dst);
+```
+// unlock the lock of srcdir and dstdir.
+```c
+void unlock2dir (struct inode* srcdir, struct inode* dstdir);
+```
+
+[SPECIFICATION of atomfs_rename]
+**System Algorithm**:
+The locking algorithm for `atomfs_rename` is divided into three distinct phases:
+
+**Phase 1: Traverse the Common Path**
+
+  * **Goal**: Find the lowest common ancestor directory (`parent`) of `srcdir` and `dstdir`.
+  * **Algorithm**:
+    1.  Acquire the lock on `root_inum`.
+    2.  Invoke `locate` to traverse the common path in a lock-coupling fashion.
+    3.  **Post-condition**: The lock on `parent` is held.
+    4.  **Error Handling**: If traversal fails (`locate` returns NULL), no locks will be held. Return -1.
+
+**Phase 2: Traverse Remaining Paths**
+
+  * **Goal**: Find the `srcdir` and `dstdir` inodes.
+  * **Algorithm**:
+    1.  **Pre-condition**: The lock on `parent` is held.
+    2.  Invoke `locate_hold` to traverse the remaining part of `srcpath` from `parent` to find `srcdir`. The lock on `parent` is held throughout.
+    3.  Invoke `locate_hold` to traverse the remaining part of `dstpath` from `parent` to find `dstdir`. The lock on `parent` is held throughout.
+    4.  Release the `parent` lock using `check_unlock` to avoid releasing it if it's the same as `srcdir` or `dstdir`.
+    5.  **Post-condition**: The locks on `srcdir` and `dstdir` are held.
+    6.  **Error Handling**: 
+        If locating `srcdir` fails, release the `parent` lock and return -1.
+        If locating `dstdir` fails, release the `parent` lock using `check_unlock` and the `srcdir` lock. Return -1.
+
+**Phase 3: Checks and Operations**
+
+  * **Goal**: Validate conditions and perform the atomic rename operation.
+  * **Algorithm**:
+    1.  **Pre-condition**: The locks on `srcdir` and `dstdir` are held.
+    2.  Validate that the source exists and that the destination is a valid and safe target for the operation via `check_src_exist_dst_delete`.
+    3.  If validation fails, return -1 (all locks will be released by `check_src_exist_dst_delete`).
+    4.  Perform the rename operation:
+        - Delete `srcname` from `srcdir` to get `srcinode`.
+        - Delete `dstname` from `dstdir` to get `dstinode`. If `dstinode` existed, dispose of it.
+        - Insert `srcinode` into `dstdir` with the name `dstname`.
+    4.  After the main operations (`inode_delete`, `inode_insert`) are complete, release the locks on `srcdir` and `dstdir` using `unlock2dir`.
+    5.  Return 0 on success.
+
+
+[SPECIFICATION of locate]
+**Pre-Condition**:
+cur is locked.
+**Post-Condition**:
+Two cases for postcondition of locate.
+Case1: If the traversal succeeds to return a target inode, only the lock of target inode is owned.
+Case2: If the return value is NULL, no lock is owned.
+
+
+[SPECIFICATION of locate_hold]
+**Pre-Condition**:
+cur is locked.
+**Post-Condition**:
+Two cases for postcondition of locate_hold.
+Case1: If the traversal succeeds to return a target inode, the lock of target inode and cur is owned. Note: in case target and cur are the same, only one lock is owned.
+Case2: if the return value is NULL, only the lock of cur is owned.
+
+
+[SPECIFICATION of check_src_exist_dst_delete]
+**Pre-Condition**:
+The locks on both `srcdir` and `dstdir` are held before calling this function.
+**Post-Condition**:
+- On Failure (return 1): All locks held upon entry and acquired during execution are released. No locks are held by this function upon return.
+- On Success (return 0):
+  - The locks on `srcdir` and `dstdir` remain held.
+  - If `dstinode` existed, its lock also remains held.
+  - The lock on `srcinode` is released before returning.
+
+
diff --git a/benchmarks/specfs_bench/data/spec/interface/atomfs_truncate.spec b/benchmarks/specfs_bench/data/spec/interface/atomfs_truncate.spec
new file mode 100644
index 00000000..005f483a
--- /dev/null
+++ b/benchmarks/specfs_bench/data/spec/interface/atomfs_truncate.spec
@@ -0,0 +1,106 @@
+[PROMPT]
+Provide complete `atomfs_truncate.c` file that implement `atomfs_truncate` operation. You can use information first from [RELY], [GUARANTEE] and [SPECIFICATION] in the first phase, then more information in the refine phase as described below. Only provide the implementation of that single function and only include `interface.h` as the header. Your output is wrapped in a C code block, and no other unrelavent code should be given.
+
+## First Prompt
+[RELY]
+```c
+int check_file(struct inode *inum);
+```
+```c
+void inode_truncate(struct inode* node, unsigned size);
+```
+// Traverse path under cur. If an inode is found, the return value is the found inode. If no inode is found, the return value is NULL. The lock of cur is released before returning, and the lock of the found inode is acquired.
+```c
+struct inode* locate(struct inode* cur, char* path[]);
+```
+```c
+#define PG_SIZE 4096
+#define INDEXTB_NUM 8192
+#define DIRTB_NUM 512
+#define MAX_FILE_LEN 256
+#define MAX_DIR_SIZE 10000000
+#define MAX_PATH_LEN 100
+#define MAX_FILE_SIZE ((unsigned)(INDEXTB_NUM * PG_SIZE))
+#define PAGE_SIZE (4096)
+```
+```c
+typedef struct inode {
+	int mutex;
+	struct mcs_mutex *impl;
+	struct mcs_node *hd;
+	unsigned maj;
+	unsigned min;
+	unsigned int mode;
+	unsigned int size;
+	struct dirtb *dir;
+	struct indextb *file;
+} inode;
+```
+```c
+extern struct inode *root_inum;
+```
+
+[GUARANTEE]
+```c
+int atomfs_truncate(char* path[], unsigned offset);
+```
+
+[SPECIFICATION]
+**Pre-Condition**:
+  * `path` must be a valid NULL-terminated array of strings representing the file path.
+  * `offset` is the target size for truncation.
+**Post-Condition**:
+**Case 1 (Successful truncation)**:
+
+  * The file identified by `path` is truncated to `offset` bytes.
+  * Returns `0` to indicate success.
+
+**Case 2 (Failure)**:
+
+  * The file system state remains unchanged.
+  * Returns `-1` if any of the following occur:
+    a) The `offset` is greater than `MAX_FILE_SIZE`.
+    b) The path traversal fails (starting from `root_inum`, following the `path` via `locate` but returns NULL).
+    c) The target inode is not a regular file (`check_file` returns non-zero).
+
+
+**Invariant**: 
+**Well-formedness of root_inum**: The global `root_inum` must point to a valid, initialized directory inode.
+
+## Refine Prompt
+[RELY]
+```c
+void lock(struct inode* inum);
+```
+```c
+void unlock(struct inode* inum);
+```
+
+[SPECIFICATION of locate]
+**Pre-Condition**:
+`cur` is locked.
+**Post-Condition**:
+If `locate` returns a non-NULL `target` inode, only the lock of `target` is owned. If `locate` returns NULL, no lock is owned.
+
+
+[SPECIFICATION of check_file]
+**Pre-Condition**:
+`inum` is locked.
+**Post-Condition**:
+If `check_file` returns 0 (success), `inum` remains locked. If `check_file` returns 1 (failure), the lock on `inum` is released.
+
+
+[SPECIFICATION of inode_truncate]
+**Pre-Condition**:
+`inum` is locked.
+**Post-Condition**:
+`inum` remains locked.
+
+
+[SPECIFICATION of atomfs_truncate]
+**Pre-Condition**:
+No lock is owned.
+**Post-Condition**:
+No lock is owned.
+
+
diff --git a/benchmarks/specfs_bench/data/spec/interface/atomfs_write.spec b/benchmarks/specfs_bench/data/spec/interface/atomfs_write.spec
new file mode 100644
index 00000000..0a61e8d6
--- /dev/null
+++ b/benchmarks/specfs_bench/data/spec/interface/atomfs_write.spec
@@ -0,0 +1,88 @@
+[PROMPT]
+Provide complete `atomfs_write.c` file that implement `atomfs_write` operation. You can use information first from [RELY], [GUARANTEE] and [SPECIFICATION] in the first phase, then more information in the refine phase as described below. Only provide the implementation of that single function and only include `interface.h` as the header. Your output is wrapped in a C code block, and no other unrelavent code should be given.
+
+## First Prompt
+[RELY]
+```c
+int check_file(struct inode *inum);
+```
+```c
+unsigned inode_write(struct inode* node, const char* buffer, unsigned len, unsigned offset);
+```
+```c
+typedef struct inode {
+	int mutex;
+	struct mcs_mutex *impl;
+	struct mcs_node *hd;
+	unsigned maj;
+	unsigned min;
+	unsigned int mode;
+	unsigned int size;
+	struct dirtb *dir;
+	struct indextb *file;
+} inode;
+```
+```c
+extern struct inode *root_inum;
+```
+// Traverse path under cur. If an inode is found, the return value is the found inode. If no inode is found, the return value is NULL. The lock of cur is released before returning, and the lock of the found inode is acquired.
+```c
+struct inode* locate(struct inode* cur, char* path[]);
+```
+
+[GUARANTEE]
+```c
+int atomfs_write(char* path[], const char* buf, unsigned size, unsigned offset);
+```
+
+[SPECIFICATION]
+**Pre-Condition**:
+`root_inum` is a valid directory inode.
+The `path` corresponds to an existing entry in the file system hierarchy rooted at `root_inum`, ensuring `locate(root_inum, path)` returns a valid non-NULL inode.
+`buf` points to a valid memory region containing at least `size` bytes.
+`size` and `offset` are non-negative integers.
+**Post-Condition**:
+The return value depends on the validity of the located inode and the write operation:
+
+**Case 1**: Starting from `root_inum`, by following `path`, an inode `inum` is found. If `check_file(inum)` indicates the inode is not writable (returns `1`), the function returns `-1`.
+
+**Case 2**: Otherwise, the function writes `size` bytes from `buf` at `offset` into the file via `inode_write` and returns the result of `inode_write`. The inode corresponding to `path` is unlocked before returning.
+
+
+**Invariant**: 
+**Well-formedness of root_inum**: The global `root_inum` must point to a valid, initialized directory inode.
+
+## Refine Prompt
+[RELY]
+```c
+void unlock(struct inode* inum);
+```
+```c
+void lock(struct inode* inum);
+```
+
+[SPECIFICATION of locate]
+**Pre-Condition**:
+cur is locked.
+**Post-Condition**:
+If target is NULL, locate would have released all locks, so no lock is owned in this case.
+If target is not NULL, only the lock of target is owned. locate would have released all other locks.
+
+
+[SPECIFICATION of atomfs_write]
+**Pre-Condition**:
+no lock is owned.
+**Post-Condition**:
+no lock is owned.
+
+
+[SPECIFICATION of check_file]
+**Pre-Condition**:
+If `inum` is not NULL, it is locked.
+**Post-Condition**:
+Failure, return 1:
+`inum` is NULL or `1num` is a directory, the lock is released and returned.
+Success, return 0:
+`inum` is still locked.
+
+
diff --git a/benchmarks/specfs_bench/data/spec/path/locate.spec b/benchmarks/specfs_bench/data/spec/path/locate.spec
new file mode 100644
index 00000000..98f157e0
--- /dev/null
+++ b/benchmarks/specfs_bench/data/spec/path/locate.spec
@@ -0,0 +1,78 @@
+[PROMPT]
+Provide complete `locate.c` file that implement `locate` operation. You can use information first from [RELY], [GUARANTEE] and [SPECIFICATION] in the first phase, then more information in the refine phase as described below. Only provide the implementation of that single function and only include `path.h` as the header. Your output is wrapped in a C code block, and no other unrelavent code should be given.
+
+## First Prompt
+[RELY]
+```c
+typedef struct inode {
+	int mutex;
+	struct mcs_mutex *impl;
+	struct mcs_node *hd;
+	unsigned maj;
+	unsigned min;
+	unsigned int mode;
+	unsigned int size;
+	struct dirtb *dir;
+	struct indextb *file;
+} inode;
+```
+```c
+struct inode *inode_find(struct inode *node, char *name);
+```
+
+[GUARANTEE]
+```c
+struct inode* locate(struct inode* cur, char* path[]);
+```
+
+[SPECIFICATION]
+**Pre-Condition**:
+- `cur` points to a valid directory inode (access to `cur->dir` is safe).
+- `path` is a valid NULL-terminated array of path component strings (each `path[i]` is a non-NULL string).
+**Post-Condition**:
+- **Case 1 (Empty path)**: If `path[0] == NULL`, returns the original locked `cur`.
+- **Case 2 (Full traversal)**: All components are successfully traversed. Returns the inode of the final path component.
+- **Case 3 (Component missing)**: A component `path[i]` is not found during traversal. Returns `NULL`.
+
+
+## Refine Prompt
+[RELY]
+```c
+void lock(struct inode* inum);
+```
+```c
+void unlock(struct inode* inum);
+```
+
+[SPECIFICATION of locate]
+**Pre-Condition**:
+cur is locked.
+**Post-Condition**:
+If the operation succeeds, the returned inode is locked. 
+If the operation fails, all locks are released.
+
+**System Algorithm**:
+1.  **Initialization**:
+    * Set a pointer `current` to the starting inode `cur`. The lock on `current` is already held.
+    * Start iterating through the `path` array from the first element.
+
+2.  **Iterative Traversal Loop**: For each `name` in the `path`:
+    * **a. Find Next Inode**: Perform the non-locking find operation: `next = inode_find(current, name)`.
+
+    * **b. Handle Path Failure**:
+        * If `next` is `NULL`, the path does not exist.
+        * To meet the failure post-condition (no locks held), release the lock on the current node: `unlock(current)`.
+        * Terminate the function and `return NULL`.
+
+    * **c. Handle Path Success (Lock Coupling)**:
+        * If `next` is a valid inode, proceed with the lock coupling sequence:
+        * **Acquire Next Lock**: First, acquire the lock on the child/next inode: `lock(next)`.
+        * **Release Current Lock**: *Only after* successfully acquiring the lock on `next`, release the lock on the parent/current inode: `unlock(current)`. This is the critical step that ensures a continuous, locked path during traversal.
+        * **Advance Pointer**: Update the `current` pointer to move down the tree: `current = next`.
+
+3.  **Successful Termination**:
+    * If the loop completes without returning `NULL`, it means the entire path has been traversed successfully.
+    * The `current` pointer now points to the final destination inode.
+    * From the last step of the loop, the lock on this final `current` inode was acquired but never released.
+    * Return the `current` pointer. The caller receives the target inode with its lock held, satisfying the success post-condition.
+
diff --git a/benchmarks/specfs_bench/data/spec/path/locate_hold.spec b/benchmarks/specfs_bench/data/spec/path/locate_hold.spec
new file mode 100644
index 00000000..955f7733
--- /dev/null
+++ b/benchmarks/specfs_bench/data/spec/path/locate_hold.spec
@@ -0,0 +1,91 @@
+[PROMPT]
+Provide complete `locate_hold.c` file that implement `locate_hold` operation. You can use information first from [RELY], [GUARANTEE] and [SPECIFICATION] in the first phase, then more information in the refine phase as described below. Only provide the implementation of that single function and only include `path.h` as the header. Your output is wrapped in a C code block, and no other unrelavent code should be given.
+
+## First Prompt
+[RELY]
+```c
+typedef struct inode {
+	int mutex;
+	struct mcs_mutex *impl;
+	struct mcs_node *hd;
+	unsigned maj;
+	unsigned min;
+	unsigned int mode;
+	unsigned int size;
+	struct dirtb *dir;
+	struct indextb *file;
+} inode;
+```
+```c
+struct inode *inode_find(struct inode *node, char *name);
+```
+// Traverse path under cur. If an inode is found, the return value is the found inode. If no inode is found, the return value is NULL. The lock of cur is released before returning, and the lock of the found inode is acquired.
+```c
+struct inode* locate(struct inode* cur, char* path[]);
+```
+```c
+typedef struct dirtb {
+	struct entry *tb[DIRTB_NUM];
+} dirtb;
+```
+
+[GUARANTEE]
+```c
+struct inode* locate_hold(struct inode *cur, char *path[]);
+```
+
+[SPECIFICATION]
+**Pre-Condition**:
+  * `cur`: A valid, non-NULL pointer to an inode representing the starting directory.
+  * `path`: A valid, NULL-terminated array of strings representing the path to traverse relative to `cur`.
+**Post-Condition**:
+  * **Case 1 (Successful Traversal)**:
+      * The traversal successfully reaches the final component specified in `path`.
+      * If `path` is empty, `cur` itself is the target.
+      * Returns a non-NULL pointer to the target inode.
+  * **Case 2 (Traversal Failure)**:
+      * An intermediate component in `path` does not exist.
+      * Returns `NULL`.
+
+**System Algorithm**:
+To traverse a sub-path starting from a given directory inode `cur`. This function is distinct from a standard `locate` because it is designed to be called when the lock on `cur` (e.g., a common ancestor directory) must be retained by the caller. The function handles the first step of the traversal itself(e.g. look up the first element of `cur`'s directory via `inode_find`) and then delegates the remainder of the traversal to the standard `locate` utility.
+
+
+## Refine Prompt
+[RELY]
+```c
+void lock(struct inode* inum);
+```
+```c
+void unlock(struct inode* inum);
+```
+
+[SPECIFICATION of locate_hold]
+**Pre-Condition**:
+The starting inode `cur` must be locked by the caller.
+**Post-Condition**:
+(Success):
+      * Let the returned inode be `target`.
+      * The lock on the initial inode `cur` **is retained**.
+      * The lock on the returned inode `target` **is acquired and held**.
+      * *Note*: If the input `path` is empty, `target` will be the same as `cur`, and only the single lock on `cur` is held.
+(Failure):
+      * Returns `NULL`.
+      * The lock on the initial inode `cur` **is retained**.
+      * No other new locks are held as a result of this function call.
+
+**System Algorithm**:
+    1.  The function starts with the lock on the current inode (`cur`) already held.
+    2.  It reads the directory contents of `cur` to find the next inode (`next_inum`).
+    3.  If `next_inum` is found, it **immediately locks `next_inum`**. At this point, locks on both the parent and child are held, preventing any other process from breaking their link.
+    4.  It then calls the `locate` function with the now-locked `next_inum`. The `locate` function is responsible for releasing the lock on the parent (`cur`) and continuing the traversal.
+    5.  If `next_inum` is **not** found, the function retains the lock on `cur` and returns `NULL`.
+
+[SPECIFICATION of locate]
+**Pre-Condition**:
+`cur` is locked.
+**Post-Condition**:
+(Success): Returns the target inode, which is now locked. All intermediate locks, including the initial lock on `cur`, have been released (i.e., it performs lock coupling).
+(Failure): Returns `NULL`. All locks acquired during the attempted traversal, including the initial lock on `cur`, have been released.
+
+
diff --git a/benchmarks/specfs_bench/data/spec/util/calculate.spec b/benchmarks/specfs_bench/data/spec/util/calculate.spec
new file mode 100644
index 00000000..dad70dce
--- /dev/null
+++ b/benchmarks/specfs_bench/data/spec/util/calculate.spec
@@ -0,0 +1,24 @@
+[PROMPT]
+Provide complete `calculate.c` file that implement `calculate` operation. You can use information from [RELY], [GUARANTEE] and [SPECIFICATION] as described below. Only provide the implementation of that single function and only include `util.h` as the header. Your output is wrapped in a C code block, and no other unrelavent code should be given.
+
+[RELY]
+```c
+char** malloc_path(unsigned len);
+```
+```c
+char* malloc_string(const char* name);
+```
+
+[GUARANTEE]
+```c
+char** calculate(char* srcpath[], char* dstpath[]);
+```
+
+[SPECIFICATION]
+**Pre-Condition**:
+- `srcpath` and `dstpath` are valid NULL-terminated arrays of strings (non-NULL pointers).
+- Each array element is a non-NULL string pointer until the final NULL terminator.
+- The functions `malloc_path` and `malloc_string` behave as described (allocate memory and return valid pointers).
+**Post-Condition**:
+Returns a NULL-terminated array `compath` containing the **longest common prefix** of `srcpath` and `dstpath`. 
+
diff --git a/benchmarks/specfs_bench/data/spec/util/dispose_inode.spec b/benchmarks/specfs_bench/data/spec/util/dispose_inode.spec
new file mode 100644
index 00000000..c6ac6af8
--- /dev/null
+++ b/benchmarks/specfs_bench/data/spec/util/dispose_inode.spec
@@ -0,0 +1,70 @@
+[PROMPT]
+Provide complete `dispose_inode.c` file that implement `dispose_inode` operation. You can use information from [RELY], [GUARANTEE] and [SPECIFICATION] as described below. Only provide the implementation of that single function and only include `util.h` as the header. Your output is wrapped in a C code block, and no other unrelavent code should be given.
+
+[RELY]
+```c
+typedef struct inode {
+	int mutex;
+	struct mcs_mutex *impl;
+	struct mcs_node *hd;
+	unsigned maj;
+	unsigned min;
+	unsigned int mode;
+	unsigned int size;
+	struct dirtb *dir;
+	struct indextb *file;
+} inode;
+```
+```c
+typedef struct entry {
+	char *name;
+	void *inum;
+	struct entry *next;
+} entry;
+```
+```c
+typedef struct indextb {
+	unsigned char *index[INDEXTB_NUM];
+} indextb;
+```
+```c
+typedef struct dirtb {
+	struct entry *tb[DIRTB_NUM];
+} dirtb;
+```
+```c
+#define FILE_MODE 1
+#define DIR_MODE 2
+#define CHR_MODE 3
+#define BLK_MODE 4
+#define SOCK_MODE 5
+#define FIFO_MODE 6
+```
+```c
+#define PG_SIZE 4096
+#define INDEXTB_NUM 8192
+#define DIRTB_NUM 512
+#define MAX_FILE_LEN 256
+#define MAX_DIR_SIZE 10000000
+#define MAX_PATH_LEN 100
+#define MAX_FILE_SIZE ((unsigned)(INDEXTB_NUM * PG_SIZE))
+#define PAGE_SIZE (4096)
+```
+```c
+//   destroy a mutex
+int mcs_mutex_destroy(mcs_mutex_t *lock);
+```
+
+[GUARANTEE]
+```c
+void dispose_inode(struct inode* inum);
+```
+
+[SPECIFICATION]
+**Pre-Condition**:
+- `inum` is a pointer to an `inode` structure.
+**Post-Condition**:
+- Remove the inode contents. If it's a directory, free the directory table. If it's a file, free the index table.
+- Destroy the mutex associated with the inode.
+- Free the inode structure itself.
+
diff --git a/benchmarks/specfs_bench/data/spec/util/fill_dir.spec b/benchmarks/specfs_bench/data/spec/util/fill_dir.spec
new file mode 100644
index 00000000..d5d59680
--- /dev/null
+++ b/benchmarks/specfs_bench/data/spec/util/fill_dir.spec
@@ -0,0 +1,62 @@
+[PROMPT]
+Provide complete `fill_dir.c` file that implement `fill_dir` operation. You can use information from [RELY], [GUARANTEE] and [SPECIFICATION] as described below. Only provide the implementation of that single function and only include `util.h` as the header. Your output is wrapped in a C code block, and no other unrelavent code should be given.
+
+[RELY]
+```c
+typedef struct inode {
+	int mutex;
+	struct mcs_mutex *impl;
+	struct mcs_node *hd;
+	unsigned maj;
+	unsigned min;
+	unsigned int mode;
+	unsigned int size;
+	struct dirtb *dir;
+	struct indextb *file;
+} inode;
+```
+```c
+typedef struct dirtb {
+	struct entry *tb[DIRTB_NUM];
+} dirtb;
+```
+```c
+#define PG_SIZE 4096
+#define INDEXTB_NUM 8192
+#define DIRTB_NUM 512
+#define MAX_FILE_LEN 256
+#define MAX_DIR_SIZE 10000000
+#define MAX_PATH_LEN 100
+#define MAX_FILE_SIZE ((unsigned)(INDEXTB_NUM * PG_SIZE))
+#define PAGE_SIZE (4096)
+```
+```c
+char* malloc_string(const char* name);
+```
+
+[GUARANTEE]
+```c
+void fill_dir(struct inode* inum, char** dircontent);
+```
+
+[SPECIFICATION]
+**Pre-Condition**:
+  * `inum` is a **valid pointer** to an initialized `inode` structure that represents a directory.
+  * `inum->dir` points to a valid `dirtable` structure.
+  * `dircontent` is a pointer to an array of `char*` that has sufficient capacity to store pointers to all entry names within the directory, plus one additional slot for a `NULL` terminator.
+**Post-Condition**:
+  * The `dircontent` array is filled with pointers to **newly allocated strings**, where each string is a copy of an entry's name from the directory.
+  * The order of names in `dircontent` corresponds to the traversal order of the directory's hash table and linked lists.
+  * The element in `dircontent` immediately following the last entry name is set to `NULL`, serving as a terminator for the list.
+  * The function **does not modify** the `inode` or its associated directory structures.
+  * The function returns `void`.
+
+**System Algorithm**:
+1.  Initialize two counters, `i` for iterating through the hash table buckets and `j` for indexing the `dircontent` array.
+2.  Iterate through each bucket of the hash table `inum->dir->tb` from index `0` to `DIRTB_NUM - 1`.
+3.  For each bucket, traverse the linked list of `entry` structures starting from the head.
+4.  For each `entry` encountered in the linked list:
+    a. Call `malloc_string` to create a memory-allocated copy of the entry's name (`walk->name`).
+    b. Store the pointer to this new string at `dircontent[j]`.
+    c. Increment the `dircontent` index `j`.
+5.  After iterating through all buckets and their corresponding linked lists, place a `NULL` pointer at `dircontent[j]` to terminate the array.
diff --git a/benchmarks/specfs_bench/data/spec/util/free_dirs.spec b/benchmarks/specfs_bench/data/spec/util/free_dirs.spec
new file mode 100644
index 00000000..0afe392b
--- /dev/null
+++ b/benchmarks/specfs_bench/data/spec/util/free_dirs.spec
@@ -0,0 +1,20 @@
+[PROMPT]
+Provide complete `free_dirs.c` file that implement `free_dirs` operation. You can use information from [RELY], [GUARANTEE] and [SPECIFICATION] as described below. Only provide the implementation of that single function and only include `util.h` as the header. Your output is wrapped in a C code block, and no other unrelavent code should be given.
+
+[GUARANTEE]
+```c
+void free_dirs(char *dirname[]);
+```
+
+[SPECIFICATION]
+**Pre-Condition**:
+  * `dirname` is a pointer to a `NULL`-terminated array of character pointers (strings).
+  * Each non-`NULL` element in the `dirname` array points to a valid block of dynamically allocated memory that can be safely passed to `free()`.
+
+**Post-Condition**:
+  * The memory pointed to by each non-`NULL` element in the `dirname` array is deallocated.
+  * The pointer to the `dirname` array itself is **not** freed.
+
+
+**System Algorithm**:
+  * The function should iterate through the `dirname` array until it encounters a `NULL` terminator. For each string it encounters, it should call `free()` to release its memory.
diff --git a/benchmarks/specfs_bench/data/spec/util/free_entry.spec b/benchmarks/specfs_bench/data/spec/util/free_entry.spec
new file mode 100644
index 00000000..2a2e0310
--- /dev/null
+++ b/benchmarks/specfs_bench/data/spec/util/free_entry.spec
@@ -0,0 +1,23 @@
+[PROMPT]
+Provide complete `free_entry.c` file that implement `free_entry` operation. You can use information from [RELY], [GUARANTEE] and [SPECIFICATION] as described below. Only provide the implementation of that single function and only include `util.h` as the header. Your output is wrapped in a C code block, and no other unrelavent code should be given.
+
+[RELY]
+```c
+typedef struct entry {
+	char *name;
+	void *inum;
+	struct entry *next;
+} entry;
+```
+
+[GUARANTEE]
+```c
+void free_entry(struct entry* en);
+```
+
+[SPECIFICATION]
+**Pre-Condition**:
+- `en` points to a valid entry structure.
+**Post-Condition**:
+- The function frees the name of the entry and the entry structure itself.
+
diff --git a/benchmarks/specfs_bench/data/spec/util/free_path.spec b/benchmarks/specfs_bench/data/spec/util/free_path.spec
new file mode 100644
index 00000000..a51016e9
--- /dev/null
+++ b/benchmarks/specfs_bench/data/spec/util/free_path.spec
@@ -0,0 +1,15 @@
+[PROMPT]
+Provide complete `free_path.c` file that implement `free_path` operation. You can use information from [RELY], [GUARANTEE] and [SPECIFICATION] as described below. Only provide the implementation of that single function and only include `util.h` as the header. Your output is wrapped in a C code block, and no other unrelavent code should be given.
+
+[GUARANTEE]
+```c
+void free_path(char** path);
+```
+
+[SPECIFICATION]
+**Pre-Condition**:
+- `path` is a pointer to a **NULL-terminated array of strings** (last element is `NULL`).
+**Post-Condition**:
+- All strings in the array (`path[0]`, `path[1]`, etc.) are deallocated using `free()`.
+- The array itself (`path`) is deallocated using `free()`.
+
diff --git a/benchmarks/specfs_bench/data/spec/util/free_readret.spec b/benchmarks/specfs_bench/data/spec/util/free_readret.spec
new file mode 100644
index 00000000..264d6f4c
--- /dev/null
+++ b/benchmarks/specfs_bench/data/spec/util/free_readret.spec
@@ -0,0 +1,23 @@
+[PROMPT]
+Provide complete `free_readret.c` file that implement `free_readret` operation. You can use information from [RELY], [GUARANTEE] and [SPECIFICATION] as described below. Only provide the implementation of that single function and only include `util.h` as the header. Your output is wrapped in a C code block, and no other unrelavent code should be given.
+
+[RELY]
+```c
+typedef struct read_ret {
+	char *buf;
+	unsigned num;
+} read_ret;
+```
+
+[GUARANTEE]
+```c
+void free_readret(struct read_ret *p);
+```
+
+[SPECIFICATION]
+**Pre-Condition**:
+  - `p` points to a valid `read_ret` structure.
+  - `p->buf` points to a dynamically allocated buffer.
+**Post-Condition**:
+  - The function frees the memory allocated for the buffer (`p->buf`) and the `read_ret` structure (`p`) itself.
+
diff --git a/benchmarks/specfs_bench/data/spec/util/getlen.spec b/benchmarks/specfs_bench/data/spec/util/getlen.spec
new file mode 100644
index 00000000..08fd89af
--- /dev/null
+++ b/benchmarks/specfs_bench/data/spec/util/getlen.spec
@@ -0,0 +1,14 @@
+[PROMPT]
+Provide complete `getlen.c` file that implement `getlen` operation. You can use information from [RELY], [GUARANTEE] and [SPECIFICATION] as described below. Only provide the implementation of that single function and only include `util.h` as the header. Your output is wrapped in a C code block, and no other unrelavent code should be given.
+
+[GUARANTEE]
+```c
+int getlen(char* path[]);
+```
+
+[SPECIFICATION]
+**Pre-Condition**:
+- `path` is a valid **NULL-terminated array** of strings
+**Post-Condition**:
+Returns the **number of non-NULL elements** in `path` before the terminating `NULL`
+
diff --git a/benchmarks/specfs_bench/data/spec/util/hash_name.spec b/benchmarks/specfs_bench/data/spec/util/hash_name.spec
new file mode 100644
index 00000000..5092acb5
--- /dev/null
+++ b/benchmarks/specfs_bench/data/spec/util/hash_name.spec
@@ -0,0 +1,28 @@
+[PROMPT]
+Provide complete `hash_name.c` file that implement `hash_name` operation. You can use information from [RELY], [GUARANTEE] and [SPECIFICATION] as described below. Only provide the implementation of that single function and only include `util.h` as the header. Your output is wrapped in a C code block, and no other unrelavent code should be given.
+
+[GUARANTEE]
+```c
+unsigned int hash_name(char* name);
+```
+
+[SPECIFICATION]
+**Pre-Condition**:
+- `name` points to a valid null-terminated string (or is `NULL`).
+**Post-Condition**:
+The function returns an unsigned integer hash value in the range `[0, 0x1ff]` (0–511). Two cases define the computation:
+
+- **Case 1 (`name` is `NULL` or empty string)**:
+  Returns `0` (initial `hash` value remains unchanged).
+
+- Case 2 (`name` points to a non-empty string):
+
+  Computes the hash through an iterative polynomial algorithm:
+
+  ```plaintext
+  hash = (hash * 131) + current_character  
+  ```
+
+  for each character until \0 (the algorithm uses a fixed seed value `131`). Final result is hash & 0x1ff (9 least significant bits).
+
+
diff --git a/benchmarks/specfs_bench/data/spec/util/lock.spec b/benchmarks/specfs_bench/data/spec/util/lock.spec
new file mode 100644
index 00000000..462985bd
--- /dev/null
+++ b/benchmarks/specfs_bench/data/spec/util/lock.spec
@@ -0,0 +1,52 @@
+[PROMPT]
+Provide complete `lock.c` file that implement `lock` operation. You can use information from [RELY], [GUARANTEE] and [SPECIFICATION] as described below. Only provide the implementation of that single function and only include `util.h` as the header. Your output is wrapped in a C code block, and no other unrelavent code should be given.
+
+[RELY]
+```c
+typedef struct inode {
+	int mutex;
+	struct mcs_mutex *impl;
+	struct mcs_node *hd;
+	unsigned maj;
+	unsigned min;
+	unsigned int mode;
+	unsigned int size;
+	struct dirtb *dir;
+	struct indextb *file;
+} inode;
+```
+```c
+typedef struct mcs_node {
+    //  ... other fields ...
+} mcs_node_t;
+```
+```c
+//  lock a mutex
+int mcs_mutex_lock(mcs_mutex_t *impl, mcs_node_t *me);
+```
+```c
+extern long syscall(long __sysno, ...);
+```
+```c
+//  The standard C library function `malloc` for dynamic memory allocation
+extern void *malloc(size_t __size)
+```
+
+[GUARANTEE]
+```c
+void lock(struct inode* inum);
+```
+
+[SPECIFICATION]
+**Pre-Condition**:
+- `inum` is a non-NULL pointer to a valid, initialized `inode` structure.
+- The `inum->impl` field must point to a valid MCS lock object.
+**Post-Condition**:
+- A new `mcs_node_t` is allocated and associated with the calling thread for this lock acquisition.
+- `inum->hd` is updated to point to the `mcs_node_t` of the calling thread.
+- `inum->mutex` is updated to the thread ID (tid) of the calling thread, marking it as the lock owner.
+
+**System Algorithm**:
+- Allocate a new MCS queue node for the current thread.
+- Invoke the underlying `mcs_mutex_lock` function to perform the atomic lock acquisition.
+- Once the lock is acquired, update the `inode`'s `hd` and `mutex` (via `syscall(SYS_gettid)`) fields to record the current thread as the owner.
diff --git a/benchmarks/specfs_bench/data/spec/util/malloc_buffer.spec b/benchmarks/specfs_bench/data/spec/util/malloc_buffer.spec
new file mode 100644
index 00000000..b349f029
--- /dev/null
+++ b/benchmarks/specfs_bench/data/spec/util/malloc_buffer.spec
@@ -0,0 +1,14 @@
+[PROMPT]
+Provide complete `malloc_buffer.c` file that implement `malloc_buffer` operation. You can use information from [RELY], [GUARANTEE] and [SPECIFICATION] as described below. Only provide the implementation of that single function and only include `util.h` as the header. Your output is wrapped in a C code block, and no other unrelavent code should be given.
+
+[GUARANTEE]
+```c
+char* malloc_buffer(unsigned len);
+```
+
+[SPECIFICATION]
+**Pre-Condition**:
+There is enough memory to allocate a buffer of length `len`.
+**Post-Condition**:
+Allocate a buffer of length `len` and return a pointer to the buffer.
+
diff --git a/benchmarks/specfs_bench/data/spec/util/malloc_dir_content.spec b/benchmarks/specfs_bench/data/spec/util/malloc_dir_content.spec
new file mode 100644
index 00000000..85a3a7b2
--- /dev/null
+++ b/benchmarks/specfs_bench/data/spec/util/malloc_dir_content.spec
@@ -0,0 +1,25 @@
+[PROMPT]
+Provide complete `malloc_dir_content.c` file that implement `malloc_dir_content` operation. You can use information from [RELY], [GUARANTEE] and [SPECIFICATION] as described below. Only provide the implementation of that single function and only include `util.h` as the header. Your output is wrapped in a C code block, and no other unrelavent code should be given.
+
+[RELY]
+```c
+//  The standard C library function `malloc` for dynamic memory allocation
+extern void *malloc(size_t __size)
+```
+
+[GUARANTEE]
+```c
+char** malloc_dir_content(unsigned size);
+```
+
+[SPECIFICATION]
+**Pre-Condition**:
+  - `size` is an unsigned integer representing the number of character pointers to allocate.
+**Post-Condition**:
+  - **Case 1: Successful Allocation**
+      - Returns a pointer (`char**`) to a newly allocated block of memory.
+      - The allocated memory is large enough to hold an array of `size` elements, where each element is a pointer to a character (`char*`).
+      - The allocated memory is not initialized.
+  - **Case 2: Allocation Failure**
+      - Returns `NULL` if the memory allocation fails.
+
diff --git a/benchmarks/specfs_bench/data/spec/util/malloc_entry.spec b/benchmarks/specfs_bench/data/spec/util/malloc_entry.spec
new file mode 100644
index 00000000..c1212ff2
--- /dev/null
+++ b/benchmarks/specfs_bench/data/spec/util/malloc_entry.spec
@@ -0,0 +1,27 @@
+[PROMPT]
+Provide complete `malloc_entry.c` file that implement `malloc_entry` operation. You can use information from [RELY], [GUARANTEE] and [SPECIFICATION] as described below. Only provide the implementation of that single function and only include `util.h` as the header. Your output is wrapped in a C code block, and no other unrelavent code should be given.
+
+[RELY]
+```c
+typedef struct entry {
+	char *name;
+	void *inum;
+	struct entry *next;
+} entry;
+```
+
+[GUARANTEE]
+```c
+struct entry *malloc_entry();
+```
+
+[SPECIFICATION]
+**Pre-Condition**:
+None.
+**Post-Condition**:
+  - **Case 1 (Successful allocation)**:
+      - Returns a valid pointer to a newly allocated memory block of size `sizeof(struct entry)`.
+      - The content of the allocated memory is uninitialized.
+  - **Case 2 (Allocation failure)**:
+      - Returns `NULL`.
+
diff --git a/benchmarks/specfs_bench/data/spec/util/malloc_getattr_ret.spec b/benchmarks/specfs_bench/data/spec/util/malloc_getattr_ret.spec
new file mode 100644
index 00000000..52fa98ce
--- /dev/null
+++ b/benchmarks/specfs_bench/data/spec/util/malloc_getattr_ret.spec
@@ -0,0 +1,50 @@
+[PROMPT]
+Provide complete `malloc_getattr_ret.c` file that implement `malloc_getattr_ret` operation. You can use information from [RELY], [GUARANTEE] and [SPECIFICATION] as described below. Only provide the implementation of that single function and only include `util.h` as the header. Your output is wrapped in a C code block, and no other unrelavent code should be given.
+
+[RELY]
+```c
+typedef struct inode {
+	int mutex;
+	struct mcs_mutex *impl;
+	struct mcs_node *hd;
+	unsigned maj;
+	unsigned min;
+	unsigned int mode;
+	unsigned int size;
+	struct dirtb *dir;
+	struct indextb *file;
+} inode;
+```
+```c
+typedef struct getattr_ret {
+	struct inode *inum;
+	unsigned mode;
+	unsigned size;
+	unsigned maj;
+	unsigned min;
+} getattr_ret;
+```
+```c
+#define FILE_MODE 1
+#define DIR_MODE 2
+#define CHR_MODE 3
+#define BLK_MODE 4
+#define SOCK_MODE 5
+#define FIFO_MODE 6
+```
+
+[GUARANTEE]
+```c
+struct getattr_ret* malloc_getattr_ret(struct inode* inum, unsigned mode, unsigned size, unsigned maj, unsigned min);
+```
+
+[SPECIFICATION]
+**Pre-Condition**:
+- `inum` is a valid pointer to an `inode` structure.
+- `mode` is a valid mode for the inode.
+- `size` is a valid size for the inode.
+- `maj` and `min` are valid major and minor device numbers.
+**Post-Condition**:
+- Returns a pointer to a `getattr_ret` structure containing the attributes of the inode.
+- Directories should have device numbers set to 0.
+
diff --git a/benchmarks/specfs_bench/data/spec/util/malloc_inode.spec b/benchmarks/specfs_bench/data/spec/util/malloc_inode.spec
new file mode 100644
index 00000000..18adbfe8
--- /dev/null
+++ b/benchmarks/specfs_bench/data/spec/util/malloc_inode.spec
@@ -0,0 +1,53 @@
+[PROMPT]
+Provide complete `malloc_inode.c` file that implement `malloc_inode` operation. You can use information from [RELY], [GUARANTEE] and [SPECIFICATION] as described below. Only provide the implementation of that single function and only include `util.h` as the header. Your output is wrapped in a C code block, and no other unrelavent code should be given.
+
+[RELY]
+```c
+typedef struct inode {
+	int mutex;
+	struct mcs_mutex *impl;
+	struct mcs_node *hd;
+	unsigned maj;
+	unsigned min;
+	unsigned int mode;
+	unsigned int size;
+	struct dirtb *dir;
+	struct indextb *file;
+} inode;
+```
+```c
+//malloc and return mcs_mutex. The return value is non-NULL.
+struct mcs_mutex * mcs_mutex_create();
+```
+
+[GUARANTEE]
+```c
+struct inode* malloc_inode(int mode, unsigned maj, unsigned min);
+```
+
+[SPECIFICATION]
+**Pre-Condition**:
+Returns a pointer to a newly allocated and initialized `inode` structure. Three initialization cases exist:
+
+1. Case 1 (Regular file) (mode != DIR_MODE):
+   - `file` field allocated and initialized to a zeroed `indextb`
+   - `dir` field remains NULL
+2. Case 2 (Directory) (mode == DIR_MODE):
+   - `dir` field allocated and initialized to a zeroed `dirtb`
+   - `file` field remains NULL
+3. Common initialization:
+   - All inode fields zeroed (The entire `inode` is zero-initialized with `memset()`) except:
+     - `mode`, `maj`, and `min` set to input arguments
+     - `impl` initialized to a new MCS mutex via `mcs_mutex_create()`
+**Post-Condition**:
+1. Case 1 (Regular file) (mode != DIR_MODE):
+   - `file` field allocated and initialized to a zeroed `indextb`
+   - `dir` field remains NULL
+2. Case 2 (Directory) (mode == DIR_MODE):
+   - `dir` field allocated and initialized to a zeroed `dirtb`
+   - `file` field remains NULL
+3. Common initialization:
+   - All inode fields zeroed (The entire `inode` is zero-initialized with `memset()`) except:
+     - `mode`, `maj`, and `min` set to input arguments
+     - `impl` initialized to a new MCS mutex via `mcs_mutex_create()`
+
diff --git a/benchmarks/specfs_bench/data/spec/util/malloc_page.spec b/benchmarks/specfs_bench/data/spec/util/malloc_page.spec
new file mode 100644
index 00000000..8226fd57
--- /dev/null
+++ b/benchmarks/specfs_bench/data/spec/util/malloc_page.spec
@@ -0,0 +1,27 @@
+[PROMPT]
+Provide complete `malloc_page.c` file that implement `malloc_page` operation. You can use information from [RELY], [GUARANTEE] and [SPECIFICATION] as described below. Only provide the implementation of that single function and only include `util.h` as the header. Your output is wrapped in a C code block, and no other unrelavent code should be given.
+
+[RELY]
+```c
+#define PG_SIZE 4096
+#define INDEXTB_NUM 8192
+#define DIRTB_NUM 512
+#define MAX_FILE_LEN 256
+#define MAX_DIR_SIZE 10000000
+#define MAX_PATH_LEN 100
+#define MAX_FILE_SIZE ((unsigned)(INDEXTB_NUM * PG_SIZE))
+#define PAGE_SIZE (4096)
+```
+
+[GUARANTEE]
+```c
+unsigned char* malloc_page();
+```
+
+[SPECIFICATION]
+**Pre-Condition**:
+None.
+**Post-Condition**:
+- Allocates a new page of memory and returns a pointer to it.
+- The allocated memory should be zero-initialized.
+
diff --git a/benchmarks/specfs_bench/data/spec/util/malloc_path.spec b/benchmarks/specfs_bench/data/spec/util/malloc_path.spec
new file mode 100644
index 00000000..39ffba46
--- /dev/null
+++ b/benchmarks/specfs_bench/data/spec/util/malloc_path.spec
@@ -0,0 +1,15 @@
+[PROMPT]
+Provide complete `malloc_path.c` file that implement `malloc_path` operation. You can use information from [RELY], [GUARANTEE] and [SPECIFICATION] as described below. Only provide the implementation of that single function and only include `util.h` as the header. Your output is wrapped in a C code block, and no other unrelavent code should be given.
+
+[GUARANTEE]
+```c
+char** malloc_path(unsigned len);
+```
+
+[SPECIFICATION]
+**Pre-Condition**:
+- `len` is a positive integer representing the length of the paths to allocate.
+
+**Post-Condition**:
+- The function returns a pointer to an array of strings (char**) representing the allocated paths. Each string is initialized to NULL.
+
diff --git a/benchmarks/specfs_bench/data/spec/util/malloc_readret.spec b/benchmarks/specfs_bench/data/spec/util/malloc_readret.spec
new file mode 100644
index 00000000..441c1154
--- /dev/null
+++ b/benchmarks/specfs_bench/data/spec/util/malloc_readret.spec
@@ -0,0 +1,23 @@
+[PROMPT]
+Provide complete `malloc_readret.c` file that implement `malloc_readret` operation. You can use information from [RELY], [GUARANTEE] and [SPECIFICATION] as described below. Only provide the implementation of that single function and only include `util.h` as the header. Your output is wrapped in a C code block, and no other unrelavent code should be given.
+
+[RELY]
+```c
+typedef struct read_ret {
+	char *buf;
+	unsigned num;
+} read_ret;
+```
+
+[GUARANTEE]
+```c
+struct read_ret* malloc_readret();
+```
+
+[SPECIFICATION]
+**Pre-Condition**:
+There is sufficient memory available to allocate a struct read_ret.
+**Post-Condition**:
+The function returns a pointer to a newly allocated struct read_ret instance. The buf field is initialized to a null pointer (0), and the num field is initialized to 0. The returned pointer is properly aligned for accessing a struct read_ret object. If memory allocation fails, the function returns NULL.
+
+
diff --git a/benchmarks/specfs_bench/data/spec/util/malloc_string.spec b/benchmarks/specfs_bench/data/spec/util/malloc_string.spec
new file mode 100644
index 00000000..cc2c60ca
--- /dev/null
+++ b/benchmarks/specfs_bench/data/spec/util/malloc_string.spec
@@ -0,0 +1,15 @@
+[PROMPT]
+Provide complete `malloc_string.c` file that implement `malloc_string` operation. You can use information from [RELY], [GUARANTEE] and [SPECIFICATION] as described below. Only provide the implementation of that single function and only include `util.h` as the header. Your output is wrapped in a C code block, and no other unrelavent code should be given.
+
+[GUARANTEE]
+```c
+char* malloc_string(const char* name);
+```
+
+[SPECIFICATION]
+**Pre-Condition**:
+- `name` is a non-NULL pointer
+**Post-Condition**:
+- Returns a pointer to newly allocated memory containing an exact copy of `name`, including the null terminator.
+- The returned pointer is always non-NULL (assumes `malloc` succeeds).
+
diff --git a/benchmarks/specfs_bench/data/spec/util/split_dirs.spec b/benchmarks/specfs_bench/data/spec/util/split_dirs.spec
new file mode 100644
index 00000000..6042022a
--- /dev/null
+++ b/benchmarks/specfs_bench/data/spec/util/split_dirs.spec
@@ -0,0 +1,44 @@
+[PROMPT]
+Provide complete `split_dirs.c` file that implement `split_dirs` operation. You can use information from [RELY], [GUARANTEE] and [SPECIFICATION] as described below. Only provide the implementation of that single function and only include `util.h` as the header. Your output is wrapped in a C code block, and no other unrelavent code should be given.
+
+[RELY]
+```c
+char* malloc_string(const char* name);
+```
+```c
+#define PG_SIZE 4096
+#define INDEXTB_NUM 8192
+#define DIRTB_NUM 512
+#define MAX_FILE_LEN 256
+#define MAX_DIR_SIZE 10000000
+#define MAX_PATH_LEN 100
+#define MAX_FILE_SIZE ((unsigned)(INDEXTB_NUM * PG_SIZE))
+#define PAGE_SIZE (4096)
+```
+
+[GUARANTEE]
+```c
+void split_dirs(const char *path, char *dirname[]);
+```
+
+[SPECIFICATION]
+**Pre-Condition**:
+  - `path`: A pointer to a valid, NULL-terminated string representing a file path (e.g., "/dir1/dir2/file").
+  - `dirname`: A pointer to an array of `char*` that is large enough to hold all the components of the `path`.
+
+**Post-Condition**:
+  - The `dirname` array is populated with pointers to newly allocated strings.
+  - Each string in `dirname` contains one component of the original `path`, in the order they appeared.
+  - The input `path` string remains unmodified.
+  - The function does not have a return value.
+
+
+**System Algorithm**:
+1.  Create a temporary, modifiable copy of the input `path` string.
+2.  Use a tokenizing function (like `strtok_r`) to iteratively split the copied string by the `/` delimiter.
+3.  For each token extracted:
+    a. Assert that the number of tokens does not exceed `MAX_PATH_LEN`.
+    b. Assert that the length of the token does not exceed `MAX_FILE_LEN`.
+    c. Use `malloc_string` to create a dynamically allocated copy of the token.
+    d. Store the pointer to this new string in the `dirname` array.
+4.  Once all tokens have been processed, free the temporary copy of the path string.
diff --git a/benchmarks/specfs_bench/data/spec/util/split_dirs_file.spec b/benchmarks/specfs_bench/data/spec/util/split_dirs_file.spec
new file mode 100644
index 00000000..258e6e27
--- /dev/null
+++ b/benchmarks/specfs_bench/data/spec/util/split_dirs_file.spec
@@ -0,0 +1,50 @@
+[PROMPT]
+Provide complete `split_dirs_file.c` file that implement `split_dirs_file` operation. You can use information from [RELY], [GUARANTEE] and [SPECIFICATION] as described below. Only provide the implementation of that single function and only include `util.h` as the header. Your output is wrapped in a C code block, and no other unrelavent code should be given.
+
+[RELY]
+```c
+char* malloc_string(const char* name);
+```
+```c
+#define PG_SIZE 4096
+#define INDEXTB_NUM 8192
+#define DIRTB_NUM 512
+#define MAX_FILE_LEN 256
+#define MAX_DIR_SIZE 10000000
+#define MAX_PATH_LEN 100
+#define MAX_FILE_SIZE ((unsigned)(INDEXTB_NUM * PG_SIZE))
+#define PAGE_SIZE (4096)
+```
+
+[GUARANTEE]
+```c
+void split_dirs_file(const char *path, char *dirname[], char *filename);
+```
+
+[SPECIFICATION]
+**Pre-Condition**:
+  - `path`: A non-NULL, null-terminated string representing an absolute file path (e.g., `/a/b/c`).
+  - `dirname`: A valid pointer to an array of `char*` pointers, initialized to `NULL`s, with a size of at least `MAX_PATH_LEN`.
+  - `filename`: A valid pointer to a character buffer, with a size of at least `MAX_FILE_LEN`.
+**Post-Condition**:
+  - **Case 1: Path contains directories and a file (e.g., `/a/b/c`)**
+      - The `dirname` array is populated with newly allocated strings for each directory component (`"a"`, `"b"`).
+      - The entry in `dirname` following the last directory component is set to `NULL`.
+      - The `filename` buffer is updated to contain the final component of the path (`"c"`).
+  - **Case 2: Path contains only a filename (e.g., `/c`)**
+      - The `dirname` array remains unmodified (all `NULL`s).
+      - The `filename` buffer is updated to contain the file's name (`"c"`).
+  - **Case 3: Path is empty or root (`/`)**
+      - Both `dirname` and `filename` remain unmodified.
+
+**System Algorithm**:
+1.  **Duplicate Path**: Create a temporary, modifiable copy of the input `path` string.
+2.  **Tokenize**: Use `strtok_r` to iteratively split the copied path by the `/` delimiter.
+3.  **Populate Directories**: For each token found:
+      - Allocate new memory for the token using `malloc_string`.
+      - Store the pointer to the new string in the next available slot of the `dirname` array.
+4.  **Isolate Filename**: After tokenization is complete:
+      - If any tokens were found, identify the last token that was added to `dirname`.
+      - Copy this last token's string content into the `filename` buffer.
+      - Free the memory for this last token within the `dirname` array and set its corresponding pointer to `NULL`.
+5.  **Cleanup**: Free the temporary copy of the path string created in step 1.
diff --git a/benchmarks/specfs_bench/data/spec/util/unlock.spec b/benchmarks/specfs_bench/data/spec/util/unlock.spec
new file mode 100644
index 00000000..6eceaa61
--- /dev/null
+++ b/benchmarks/specfs_bench/data/spec/util/unlock.spec
@@ -0,0 +1,48 @@
+[PROMPT]
+Provide complete `unlock.c` file that implement `unlock` operation. You can use information from [RELY], [GUARANTEE] and [SPECIFICATION] as described below. Only provide the implementation of that single function and only include `util.h` as the header. Your output is wrapped in a C code block, and no other unrelavent code should be given.
+
+[RELY]
+```c
+typedef struct inode {
+	int mutex;
+	struct mcs_mutex *impl;
+	struct mcs_node *hd;
+	unsigned maj;
+	unsigned min;
+	unsigned int mode;
+	unsigned int size;
+	struct dirtb *dir;
+	struct indextb *file;
+} inode;
+```
+```c
+typedef struct mcs_node {
+    //  ... other fields ...
+} mcs_node_t;
+```
+```c
+//   unlock the MCS mutex, `me` will be changed to point to the next node in the queue
+void mcs_mutex_unlock(mcs_mutex_t *impl, mcs_node_t *me);
+```
+
+[GUARANTEE]
+```c
+void unlock(struct inode* inum);
+```
+
+[SPECIFICATION]
+**Pre-Condition**:
+  - `inum` points to a valid `inode` structure that has been previously initialized.
+  - The `inode` lock associated with `inum` is currently held by the calling thread.
+  - `inum->hd` points to the valid `mcs_node_t` that was used by the current thread to acquire the lock.
+**Post-Condition**:
+  - The MCS lock associated with the `inode` is released, potentially allowing another waiting thread to acquire it.
+  - The `inum->mutex` flag is cleared to 0.
+  - The memory allocated for the `mcs_node_t` (pointed to by `inum->hd`) is deallocated.
+  - The function has no return value.
+
+**System Algorithm**:
+1. Acquire the pointer to the `mcs_node_t` structure from the `hd` field of the `inode`.
+2. Clear the `mutex` field of the `inode`.
+3. Call `mcs_mutex_unlock` with the `impl` field of the `inode` and the acquired `mcs_node_t` pointer to release the lock.
+4. Free the memory allocated for the `mcs_node_t` structure.
diff --git a/benchmarks/specfs_bench/data/spec/util/unlock2dir.spec b/benchmarks/specfs_bench/data/spec/util/unlock2dir.spec
new file mode 100644
index 00000000..7ca516ff
--- /dev/null
+++ b/benchmarks/specfs_bench/data/spec/util/unlock2dir.spec
@@ -0,0 +1,34 @@
+[PROMPT]
+Provide complete `unlock2dir.c` file that implement `unlock2dir` operation. You can use information from [RELY], [GUARANTEE] and [SPECIFICATION] as described below. Only provide the implementation of that single function and only include `util.h` as the header. Your output is wrapped in a C code block, and no other unrelavent code should be given.
+
+[RELY]
+```c
+typedef struct inode {
+	int mutex;
+	struct mcs_mutex *impl;
+	struct mcs_node *hd;
+	unsigned maj;
+	unsigned min;
+	unsigned int mode;
+	unsigned int size;
+	struct dirtb *dir;
+	struct indextb *file;
+} inode;
+```
+```c
+void unlock(struct inode* inum);
+```
+
+[GUARANTEE]
+```c
+void unlock2dir (struct inode* srcdir, struct inode* dstdir);
+```
+
+[SPECIFICATION]
+**Pre-Condition**:
+- `srcdir` is the source directory inode to be unlocked.
+- `dstdir` is the destination directory inode to be unlocked.
+**Post-Condition**:
+- The function releases the locks of both the source and destination directory inodes.
+- If `srcdir` and `dstdir` are the same, only one lock is released.
+
diff --git a/benchmarks/specfs_bench/env.toml.example b/benchmarks/specfs_bench/env.toml.example
new file mode 100644
index 00000000..b0143794
--- /dev/null
+++ b/benchmarks/specfs_bench/env.toml.example
@@ -0,0 +1,5 @@
+[llm]
+
+OPENAI_API_KEY = "your_key_here" 
+
+OPENAI_API_BASE = "your_url_here"
\ No newline at end of file
diff --git a/benchmarks/specfs_bench/install.sh b/benchmarks/specfs_bench/install.sh
new file mode 100755
index 00000000..67f8074c
--- /dev/null
+++ b/benchmarks/specfs_bench/install.sh
@@ -0,0 +1,18 @@
+#!/bin/bash
+
+set -e
+
+if [ -d ".venv" ]; then
+	echo "==> .venv already exists, skipping creation."
+else
+	echo "==> Creating .venv ..."
+	python3 -m venv .venv
+fi
+
+source .venv/bin/activate
+pip install --upgrade pip
+pip install -r requirements.txt
+deactivate
+
+echo "✅ SpecFS benchmark environment is set up successfully."
+echo "👉 To activate the virtual environment, run: source .venv/bin/activate"
diff --git a/benchmarks/specfs_bench/requirements.txt b/benchmarks/specfs_bench/requirements.txt
new file mode 100644
index 00000000..03321fcc
--- /dev/null
+++ b/benchmarks/specfs_bench/requirements.txt
@@ -0,0 +1,4 @@
+litellm==1.77.5
+requests
+azure-identity
+tomli
diff --git a/benchmarks/specfs_bench/run.sh b/benchmarks/specfs_bench/run.sh
new file mode 100755
index 00000000..89d8020f
--- /dev/null
+++ b/benchmarks/specfs_bench/run.sh
@@ -0,0 +1,25 @@
+#!/bin/bash
+
+set -e
+
+if [ $# -lt 1 ] || [ $# -gt 2 ]; then
+	echo "Usage: $0 <model_name> [judge_model_name]"
+	echo "Example: $0 gpt-4o"
+	echo "Example: $0 openai/deepseek-chat gpt-4o"
+	exit 1
+fi
+
+MODEL_NAME="$1"
+JUDGE_MODEL_NAME="${2:-$1}"
+
+source .venv/bin/activate
+echo "==> Running SpecFS benchmark"
+echo "==> Generator model: ${MODEL_NAME}"
+echo "==> Judge model: ${JUDGE_MODEL_NAME}"
+
+python src/main.py \
+	--model_name "${MODEL_NAME}" \
+	--judge_model_name "${JUDGE_MODEL_NAME}"
+
+deactivate
+
diff --git a/benchmarks/specfs_bench/src/evaluator.py b/benchmarks/specfs_bench/src/evaluator.py
new file mode 100644
index 00000000..53366899
--- /dev/null
+++ b/benchmarks/specfs_bench/src/evaluator.py
@@ -0,0 +1,83 @@
+"""LLM-as-a-judge evaluator for SpecFS benchmark."""
+
+from __future__ import annotations
+
+import json
+import re
+from dataclasses import dataclass
+from typing import Any
+
+from sdk.llm import LLM
+
+
+@dataclass
+class JudgeResult:
+    """Single judge result."""
+
+    score: float
+    verdict: str
+    summary: str
+    differences: list[str]
+    raw_judge_response: str
+
+
+class JudgeEvaluator:
+    """Evaluate generated C code against ground truth using an LLM judge."""
+
+    def __init__(self, model_name: str, prompt_template: str) -> None:
+        self.model_name = model_name
+        self.prompt_template = prompt_template
+
+    def _build_prompt(self, spec_text: str, generated_code: str, ground_truth_code: str) -> str:
+        return (
+            self.prompt_template.replace('{{SPEC_CONTENT}}', spec_text)
+            .replace('{{GENERATED_CODE}}', generated_code)
+            .replace('{{GROUND_TRUTH_CODE}}', ground_truth_code)
+        )
+
+    def _parse_json(self, text: str) -> dict[str, Any]:
+        """Parse JSON from plain text or fenced code block."""
+        try:
+            return json.loads(text)
+        except json.JSONDecodeError:
+            pass
+
+        match = re.search(r'```json\s*(\{.*?\})\s*```', text, re.DOTALL)
+        if match:
+            try:
+                return json.loads(match.group(1))
+            except json.JSONDecodeError:
+                return {}
+        return {}
+
+    @staticmethod
+    def _normalize_score(score: Any) -> float:
+        try:
+            value = float(score)
+        except (TypeError, ValueError):
+            return 0.0
+        return max(0.0, min(10.0, value))
+
+    def eval_case(self, spec_text: str, generated_code: str, ground_truth_code: str) -> JudgeResult:
+        """Judge one generated file."""
+        llm = LLM(engine=self.model_name, temperature=0.0, json_format=True)
+        prompt = self._build_prompt(spec_text=spec_text, generated_code=generated_code, ground_truth_code=ground_truth_code)
+        raw_response = llm.query(prompt)
+
+        parsed = self._parse_json(raw_response)
+        score = self._normalize_score(parsed.get('score'))
+        verdict = str(parsed.get('verdict', 'unknown')).strip() or 'unknown'
+        summary = str(parsed.get('summary', '')).strip()
+
+        diffs = parsed.get('differences', [])
+        if not isinstance(diffs, list):
+            diffs = [str(diffs)]
+        differences = [str(item).strip() for item in diffs if str(item).strip()]
+
+        return JudgeResult(
+            score=score,
+            verdict=verdict,
+            summary=summary,
+            differences=differences,
+            raw_judge_response=raw_response,
+        )
diff --git a/benchmarks/specfs_bench/src/genspec_prompt.md b/benchmarks/specfs_bench/src/genspec_prompt.md
new file mode 100644
index 00000000..6967ea59
--- /dev/null
+++ b/benchmarks/specfs_bench/src/genspec_prompt.md
@@ -0,0 +1,18 @@
+You need to generate code according to provided specification and comments.
+
+The following will introduce the expected input (prompts) and the expected output.
+
+Your input (the prompt) should be composed of four parts (in most cases): [PROMPT], [RELY], [GUARANTEE], and [SPECIFICATION].
+
+The descriptions different input parts are:
+* [PROMPT] represents the overall requirement for an LLM to generate the source code.
+* [RELY] clearly lists the predefined structures/functions from other modules that can be used for generating the source code. This is to avoid re-implementing functions, data structures, and variables that have already been implemented in other modules, ensuring correctness and modularity.
+* [GUARANTEE] provides the precise function signature that needs to be generated, along with specific requirements like the locking status, which the implemented source code (referred to as a single module) should meet. This is used to provide public functions, data structures, and variables for other modules to use, achieving correctness and modularity.
+* [SPECIFICATION] describes the functionality of the source code in this module (from the input). You should follow Hoare Logic and provide the pre-condition and post-condition for each function.
+
+For the output, only return a code block without any explanations or additional information.
+
+Notably:
+* you are generating a single module, instead of a whole project. So it is OK that you will directly use pre-defined functions and data structures defined in other modules (which are described in [Rely]), and do not generate those pre-defined modules and data structures already implemented in other modules, which will make the generation wrong!
+
+{{SPEC_CONTENT}}
\ No newline at end of file
diff --git a/benchmarks/specfs_bench/src/judge_prompt.md b/benchmarks/specfs_bench/src/judge_prompt.md
new file mode 100644
index 00000000..ee665fba
--- /dev/null
+++ b/benchmarks/specfs_bench/src/judge_prompt.md
@@ -0,0 +1,26 @@
+[TASK]
+You are an impartial judge for C code generation benchmark.
+Compare `GENERATED_CODE` against `GROUND_TRUTH_CODE` under the same `SPEC_CONTENT`.
+
+[SCORING]
+- score: 0-10 (10 = fully equivalent and correct)
+- Focus on functional correctness first; style is secondary.
+- Penalize missing edge-case handling, contract violations, unsafe memory handling, incorrect return behavior, and broken API usage.
+
+[OUTPUT_FORMAT]
+Return JSON ONLY (no markdown, no extra text):
+{
+	"score": <number 0-10>,
+	"verdict": "pass" | "partial" | "fail",
+	"summary": "short rationale",
+	"differences": ["difference 1", "difference 2"]
+}
+
+[SPEC_CONTENT]
+{{SPEC_CONTENT}}
+
+[GENERATED_CODE]
+{{GENERATED_CODE}}
+
+[GROUND_TRUTH_CODE]
+{{GROUND_TRUTH_CODE}}
diff --git a/benchmarks/specfs_bench/src/main.py b/benchmarks/specfs_bench/src/main.py
new file mode 100644
index 00000000..c6a2c9c7
--- /dev/null
+++ b/benchmarks/specfs_bench/src/main.py
@@ -0,0 +1,303 @@
+"""Main entry point for the SpecFS benchmark."""
+
+from __future__ import annotations
+
+import argparse
+import json
+import os
+import sys
+from datetime import datetime
+from pathlib import Path
+from typing import Any
+
+sys.path.append(os.path.abspath(os.path.join(os.path.dirname(__file__), '../../../')))
+
+from sdk.executor import SimpleExecutor
+from sdk.logger import logger
+from sdk.utils import set_llm_endpoint_from_config
+
+from evaluator import JudgeEvaluator
+
+
+def resolve_config_path(benchmark_root: Path) -> Path | None:
+    """Resolve env config path, preferring local benchmark config."""
+    local_config = benchmark_root / 'env.toml'
+    workspace_config = benchmark_root.parent / 'env.toml'
+    if local_config.exists():
+        return local_config
+    if workspace_config.exists():
+        return workspace_config
+    return None
+
+
+def read_text(path: Path) -> str:
+    """Read UTF-8 text."""
+    return path.read_text(encoding='utf-8')
+
+
+def discover_spec_files(spec_root: Path) -> list[Path]:
+    """Discover all .spec files recursively."""
+    return sorted(spec_root.rglob('*.spec'))
+
+
+def make_default_output_dir(model_name: str, judge_model_name: str) -> Path:
+    """Build default output directory with benchmark convention."""
+    timestamp = datetime.now().strftime('%Y-%m-%d_%H-%M-%S')
+    safe_model = model_name.replace('/', '_')
+    safe_judge_model = judge_model_name.replace('/', '_')
+    return Path('./outputs') / f'specfsbench__{safe_model}__judge_{safe_judge_model}__{timestamp}'
+
+
+def rel_code_path_for_spec(spec_root: Path, spec_path: Path) -> Path:
+    """Map spec file path to expected relative code path under data/code."""
+    rel = spec_path.relative_to(spec_root)
+    return rel.with_suffix('.c')
+
+
+def load_prompt(prompt_file: Path) -> str:
+    """Load prompt template."""
+    text = read_text(prompt_file).strip()
+    if text:
+        return text
+    raise ValueError(f'Prompt template is empty. Please provide a valid prompt in {prompt_file}.')
+
+
+def run_generation(
+    spec_files: list[Path],
+    spec_root: Path,
+    output_dir: Path,
+    model_name: str,
+    generation_prompt_template: str,
+) -> list[dict[str, Any]]:
+    """Run spec-to-code generation for each spec file."""
+    generated_root = output_dir / 'generated'
+    generated_root.mkdir(parents=True, exist_ok=True)
+
+    executor = SimpleExecutor(model_name, "")
+    results: list[dict[str, Any]] = []
+
+    for index, spec_path in enumerate(spec_files, start=1):
+        rel_code_path = rel_code_path_for_spec(spec_root, spec_path)
+        output_code_path = generated_root / rel_code_path
+        output_code_path.parent.mkdir(parents=True, exist_ok=True)
+
+        spec_text = read_text(spec_path)
+        prompt = generation_prompt_template.replace('{{SPEC_CONTENT}}', spec_text)
+
+        record: dict[str, Any] = {
+            'index': index,
+            'spec_path': str(spec_path),
+            'relative_code_path': str(rel_code_path),
+            'generated_code_path': str(output_code_path),
+            'status': 'success',
+        }
+
+        try:
+            generated_code = executor.run(prompt, lang='c')
+            output_code_path.write_text(generated_code, encoding='utf-8')
+            record['generated_chars'] = len(generated_code)
+            executor.LLM.reset()
+        except Exception as exc:  # noqa: BLE001
+            record['status'] = 'generation_error'
+            record['error'] = str(exc)
+            logger.error('Generation failed for %s: %s', spec_path, exc)
+
+        results.append(record)
+
+    return results
+
+
+def run_judging(
+    generation_results: list[dict[str, Any]],
+    code_root: Path,
+    judge_model_name: str,
+    judge_prompt_template: str,
+) -> list[dict[str, Any]]:
+    """Run LLM judge over generated code and ground truth code."""
+    evaluator = JudgeEvaluator(
+        model_name=judge_model_name,
+        prompt_template=judge_prompt_template,
+    )
+
+    judge_results: list[dict[str, Any]] = []
+    for item in generation_results:
+        spec_path = Path(item['spec_path'])
+        rel_code_path = Path(item['relative_code_path'])
+        generated_code_path = Path(item['generated_code_path'])
+        ground_truth_path = code_root / rel_code_path
+
+        result: dict[str, Any] = {
+            'spec_path': str(spec_path),
+            'relative_code_path': str(rel_code_path),
+            'generated_code_path': str(generated_code_path),
+            'ground_truth_path': str(ground_truth_path),
+            'status': 'success',
+            'score': None,
+            'verdict': None,
+            'summary': None,
+            'differences': [],
+        }
+
+        if item.get('status') != 'success':
+            result['status'] = 'skip_generation_error'
+            judge_results.append(result)
+            continue
+
+        if not generated_code_path.exists():
+            result['status'] = 'missing_generated'
+            judge_results.append(result)
+            continue
+
+        if not ground_truth_path.exists():
+            result['status'] = 'missing_ground_truth'
+            judge_results.append(result)
+            continue
+
+        try:
+            spec_text = read_text(spec_path)
+            generated_code = read_text(generated_code_path)
+            ground_truth_code = read_text(ground_truth_path)
+            judge_out = evaluator.eval_case(spec_text=spec_text, generated_code=generated_code, ground_truth_code=ground_truth_code)
+
+            result['score'] = judge_out.score
+            result['verdict'] = judge_out.verdict
+            result['summary'] = judge_out.summary
+            result['differences'] = judge_out.differences
+            result['raw_judge_response'] = judge_out.raw_judge_response
+        except Exception as exc:  # noqa: BLE001
+            result['status'] = 'judge_error'
+            result['error'] = str(exc)
+            logger.error('Judge failed for %s: %s', spec_path, exc)
+
+        judge_results.append(result)
+
+    return judge_results
+
+
+def write_jsonl(path: Path, records: list[dict[str, Any]]) -> None:
+    """Write records to jsonl."""
+    with path.open('w', encoding='utf-8') as output_file:
+        for item in records:
+            output_file.write(json.dumps(item, ensure_ascii=False) + '\\n')
+
+
+def build_summary(
+    model_name: str,
+    judge_model_name: str,
+    generation_results: list[dict[str, Any]],
+    judge_results: list[dict[str, Any]],
+) -> dict[str, Any]:
+    """Build summary stats."""
+    generation_success = [item for item in generation_results if item.get('status') == 'success']
+    generation_errors = [item for item in generation_results if item.get('status') != 'success']
+
+    judged = [item for item in judge_results if item.get('status') == 'success' and isinstance(item.get('score'), (int, float))]
+    missing_ground_truth = [item for item in judge_results if item.get('status') == 'missing_ground_truth']
+    judge_errors = [item for item in judge_results if item.get('status') == 'judge_error']
+    skipped_generation = [item for item in judge_results if item.get('status') == 'skip_generation_error']
+
+    avg_score = sum(float(item['score']) for item in judged) / len(judged) if judged else 0.0
+
+    summary = {
+        'model_name': model_name,
+        'judge_model_name': judge_model_name,
+        'timestamp': datetime.now().isoformat(),
+        'generation': {
+            'total_specs': len(generation_results),
+            'success_count': len(generation_success),
+            'error_count': len(generation_errors),
+        },
+        'judge': {
+            'total_cases': len(judge_results),
+            'judged_count': len(judged),
+            'missing_ground_truth_count': len(missing_ground_truth),
+            'judge_error_count': len(judge_errors),
+            'skipped_generation_error_count': len(skipped_generation),
+            'avg_score_10': round(avg_score, 4),
+            'avg_score_100': round(avg_score * 10, 2),
+        },
+    }
+    return summary
+
+
+def main(args: argparse.Namespace) -> None:
+    """Run benchmark pipeline."""
+    current_dir = Path(__file__).resolve().parent
+    benchmark_root = current_dir.parent
+
+    config_path = resolve_config_path(benchmark_root)
+    if config_path is not None:
+        logger.info('Loading config from: %s', config_path)
+        set_llm_endpoint_from_config(str(config_path))
+    else:
+        logger.warning('No env.toml found. Relying on environment variables only.')
+
+    spec_root = (benchmark_root / args.spec_dir).resolve()
+    code_root = (benchmark_root / args.code_dir).resolve()
+
+    if not spec_root.exists():
+        raise FileNotFoundError(f'Spec directory not found: {spec_root}')
+
+    output_dir = Path(args.output_dir).resolve() if args.output_dir else make_default_output_dir(args.model_name, args.judge_model_name).resolve()
+    output_dir.mkdir(parents=True, exist_ok=True)
+
+    spec_files = discover_spec_files(spec_root)
+    if args.max_cases is not None and args.max_cases > 0:
+        spec_files = spec_files[: args.max_cases]
+
+    generation_prompt_file = current_dir / 'genspec_prompt.md'
+    judge_prompt_file = current_dir / 'judge_prompt.md'
+    generation_prompt = load_prompt(generation_prompt_file)
+    judge_prompt = load_prompt(judge_prompt_file)
+
+    logger.info('Discovered %s spec files.', len(spec_files))
+
+    generation_results = run_generation(
+        spec_files=spec_files,
+        spec_root=spec_root,
+        output_dir=output_dir,
+        model_name=args.model_name,
+        generation_prompt_template=generation_prompt,
+    )
+    write_jsonl(output_dir / 'generation_results.jsonl', generation_results)
+
+    judge_results: list[dict[str, Any]] = []
+    if not args.skip_judge:
+        judge_results = run_judging(
+            generation_results=generation_results,
+            code_root=code_root,
+            judge_model_name=args.judge_model_name,
+            judge_prompt_template=judge_prompt,
+        )
+        write_jsonl(output_dir / 'judge_results.jsonl', judge_results)
+
+    summary = build_summary(
+        model_name=args.model_name,
+        judge_model_name=args.judge_model_name,
+        generation_results=generation_results,
+        judge_results=judge_results,
+    )
+
+    with (output_dir / 'summary.json').open('w', encoding='utf-8') as summary_file:
+        json.dump(summary, summary_file, ensure_ascii=False, indent=2)
+
+    logger.info('SpecFS benchmark finished.')
+    logger.info('Outputs: %s', output_dir)
+    logger.info('Summary: %s', summary)
+
+
+if __name__ == '__main__':
+    parser = argparse.ArgumentParser(description='SpecFS Benchmark')
+    parser.add_argument('-m', '--model_name', required=True, help='Model name for code generation')
+    parser.add_argument('--judge_model_name', default=None, help='Model name for judge (default: same as model_name)')
+    parser.add_argument('-o', '--output_dir', default=None, help='Output directory path')
+    parser.add_argument('--spec_dir', default='data/spec', help='Relative path to spec directory')
+    parser.add_argument('--code_dir', default='data/code', help='Relative path to ground-truth code directory')
+    parser.add_argument('--max_cases', type=int, default=None, help='Optional max number of specs to run')
+    parser.add_argument('--skip_judge', action='store_true', help='Skip judge stage')
+
+    args = parser.parse_args()
+    if args.judge_model_name is None:
+        args.judge_model_name = args.model_name
+
+    main(args)
diff --git a/benchmarks/specfs_bench/tests/__init__.py b/benchmarks/specfs_bench/tests/__init__.py
new file mode 100644
index 00000000..e69de29b