From b92022c2d100a6464dffc580dd5df83dc5c26a13 Mon Sep 17 00:00:00 2001 From: HarryZ Date: Sun, 8 Mar 2026 22:48:47 +0800 Subject: [PATCH 1/5] init specfs benchmark --- benchmarks/specfs_bench/README.md | 50 +++ .../specfs_bench/data/spec/common.header | 67 ++++ .../specfs_bench/data/spec/file/file.header | 5 + .../data/spec/file/file_allocate.spec | 50 +++ .../data/spec/file/file_clear.spec | 36 +++ .../data/spec/file/file_read.spec | 36 +++ .../data/spec/file/file_write.spec | 55 ++++ .../specfs_bench/data/spec/inode/inode.header | 7 + .../data/spec/inode/inode_delete.spec | 51 +++ .../data/spec/inode/inode_find.spec | 48 +++ .../data/spec/inode/inode_insert.spec | 51 +++ .../data/spec/inode/inode_read.spec | 56 ++++ .../data/spec/inode/inode_truncate.spec | 38 +++ .../data/spec/inode/inode_write.spec | 53 +++ .../data/spec/interface-util/check_del.spec | 77 +++++ .../data/spec/interface-util/check_dir.spec | 65 ++++ .../data/spec/interface-util/check_file.spec | 63 ++++ .../data/spec/interface-util/check_ins.spec | 72 +++++ .../data/spec/interface-util/check_open.spec | 70 ++++ .../check_src_exist_dst_delete.spec | 110 +++++++ .../spec/interface-util/check_unlock.spec | 25 ++ .../spec/interface-util/interface-util.header | 8 + .../data/spec/interface/atomfs_del.spec | 90 ++++++ .../data/spec/interface/atomfs_getattr.spec | 81 +++++ .../data/spec/interface/atomfs_ins.spec | 95 ++++++ .../data/spec/interface/atomfs_open.spec | 85 +++++ .../data/spec/interface/atomfs_read.spec | 89 +++++ .../data/spec/interface/atomfs_readdir.spec | 97 ++++++ .../data/spec/interface/atomfs_rename.spec | 196 +++++++++++ .../data/spec/interface/atomfs_truncate.spec | 106 ++++++ .../data/spec/interface/atomfs_write.spec | 88 +++++ .../data/spec/interface/interface.header | 10 + .../specfs_bench/data/spec/path/locate.spec | 78 +++++ .../data/spec/path/locate_hold.spec | 91 ++++++ .../specfs_bench/data/spec/path/path.header | 3 + .../data/spec/util/calculate.spec | 24 ++ .../data/spec/util/dispose_inode.spec | 70 ++++ .../specfs_bench/data/spec/util/fill_dir.spec | 62 ++++ .../data/spec/util/free_dirs.spec | 20 ++ .../data/spec/util/free_entry.spec | 23 ++ .../data/spec/util/free_path.spec | 15 + .../data/spec/util/free_readret.spec | 23 ++ .../specfs_bench/data/spec/util/getlen.spec | 14 + .../data/spec/util/hash_name.spec | 28 ++ .../specfs_bench/data/spec/util/lock.spec | 52 +++ .../data/spec/util/malloc_buffer.spec | 14 + .../data/spec/util/malloc_dir_content.spec | 25 ++ .../data/spec/util/malloc_entry.spec | 27 ++ .../data/spec/util/malloc_getattr_ret.spec | 50 +++ .../data/spec/util/malloc_inode.spec | 53 +++ .../data/spec/util/malloc_page.spec | 27 ++ .../data/spec/util/malloc_path.spec | 15 + .../data/spec/util/malloc_readret.spec | 23 ++ .../data/spec/util/malloc_string.spec | 15 + .../data/spec/util/split_dirs.spec | 44 +++ .../data/spec/util/split_dirs_file.spec | 50 +++ .../specfs_bench/data/spec/util/unlock.spec | 48 +++ .../data/spec/util/unlock2dir.spec | 34 ++ .../specfs_bench/data/spec/util/util.header | 24 ++ benchmarks/specfs_bench/env.toml.example | 5 + benchmarks/specfs_bench/install.sh | 18 ++ benchmarks/specfs_bench/requirements.txt | 4 + benchmarks/specfs_bench/run.sh | 25 ++ benchmarks/specfs_bench/src/evaluator.py | 84 +++++ benchmarks/specfs_bench/src/genspec_prompt.md | 18 ++ benchmarks/specfs_bench/src/judge_prompt.md | 26 ++ benchmarks/specfs_bench/src/main.py | 304 ++++++++++++++++++ benchmarks/specfs_bench/tests/__init__.py | 0 68 files changed, 3466 insertions(+) create mode 100644 benchmarks/specfs_bench/README.md create mode 100644 benchmarks/specfs_bench/data/spec/common.header create mode 100644 benchmarks/specfs_bench/data/spec/file/file.header create mode 100644 benchmarks/specfs_bench/data/spec/file/file_allocate.spec create mode 100644 benchmarks/specfs_bench/data/spec/file/file_clear.spec create mode 100644 benchmarks/specfs_bench/data/spec/file/file_read.spec create mode 100644 benchmarks/specfs_bench/data/spec/file/file_write.spec create mode 100644 benchmarks/specfs_bench/data/spec/inode/inode.header create mode 100644 benchmarks/specfs_bench/data/spec/inode/inode_delete.spec create mode 100644 benchmarks/specfs_bench/data/spec/inode/inode_find.spec create mode 100644 benchmarks/specfs_bench/data/spec/inode/inode_insert.spec create mode 100644 benchmarks/specfs_bench/data/spec/inode/inode_read.spec create mode 100644 benchmarks/specfs_bench/data/spec/inode/inode_truncate.spec create mode 100644 benchmarks/specfs_bench/data/spec/inode/inode_write.spec create mode 100644 benchmarks/specfs_bench/data/spec/interface-util/check_del.spec create mode 100644 benchmarks/specfs_bench/data/spec/interface-util/check_dir.spec create mode 100644 benchmarks/specfs_bench/data/spec/interface-util/check_file.spec create mode 100644 benchmarks/specfs_bench/data/spec/interface-util/check_ins.spec create mode 100644 benchmarks/specfs_bench/data/spec/interface-util/check_open.spec create mode 100644 benchmarks/specfs_bench/data/spec/interface-util/check_src_exist_dst_delete.spec create mode 100644 benchmarks/specfs_bench/data/spec/interface-util/check_unlock.spec create mode 100644 benchmarks/specfs_bench/data/spec/interface-util/interface-util.header create mode 100644 benchmarks/specfs_bench/data/spec/interface/atomfs_del.spec create mode 100644 benchmarks/specfs_bench/data/spec/interface/atomfs_getattr.spec create mode 100644 benchmarks/specfs_bench/data/spec/interface/atomfs_ins.spec create mode 100644 benchmarks/specfs_bench/data/spec/interface/atomfs_open.spec create mode 100644 benchmarks/specfs_bench/data/spec/interface/atomfs_read.spec create mode 100644 benchmarks/specfs_bench/data/spec/interface/atomfs_readdir.spec create mode 100644 benchmarks/specfs_bench/data/spec/interface/atomfs_rename.spec create mode 100644 benchmarks/specfs_bench/data/spec/interface/atomfs_truncate.spec create mode 100644 benchmarks/specfs_bench/data/spec/interface/atomfs_write.spec create mode 100644 benchmarks/specfs_bench/data/spec/interface/interface.header create mode 100644 benchmarks/specfs_bench/data/spec/path/locate.spec create mode 100644 benchmarks/specfs_bench/data/spec/path/locate_hold.spec create mode 100644 benchmarks/specfs_bench/data/spec/path/path.header create mode 100644 benchmarks/specfs_bench/data/spec/util/calculate.spec create mode 100644 benchmarks/specfs_bench/data/spec/util/dispose_inode.spec create mode 100644 benchmarks/specfs_bench/data/spec/util/fill_dir.spec create mode 100644 benchmarks/specfs_bench/data/spec/util/free_dirs.spec create mode 100644 benchmarks/specfs_bench/data/spec/util/free_entry.spec create mode 100644 benchmarks/specfs_bench/data/spec/util/free_path.spec create mode 100644 benchmarks/specfs_bench/data/spec/util/free_readret.spec create mode 100644 benchmarks/specfs_bench/data/spec/util/getlen.spec create mode 100644 benchmarks/specfs_bench/data/spec/util/hash_name.spec create mode 100644 benchmarks/specfs_bench/data/spec/util/lock.spec create mode 100644 benchmarks/specfs_bench/data/spec/util/malloc_buffer.spec create mode 100644 benchmarks/specfs_bench/data/spec/util/malloc_dir_content.spec create mode 100644 benchmarks/specfs_bench/data/spec/util/malloc_entry.spec create mode 100644 benchmarks/specfs_bench/data/spec/util/malloc_getattr_ret.spec create mode 100644 benchmarks/specfs_bench/data/spec/util/malloc_inode.spec create mode 100644 benchmarks/specfs_bench/data/spec/util/malloc_page.spec create mode 100644 benchmarks/specfs_bench/data/spec/util/malloc_path.spec create mode 100644 benchmarks/specfs_bench/data/spec/util/malloc_readret.spec create mode 100644 benchmarks/specfs_bench/data/spec/util/malloc_string.spec create mode 100644 benchmarks/specfs_bench/data/spec/util/split_dirs.spec create mode 100644 benchmarks/specfs_bench/data/spec/util/split_dirs_file.spec create mode 100644 benchmarks/specfs_bench/data/spec/util/unlock.spec create mode 100644 benchmarks/specfs_bench/data/spec/util/unlock2dir.spec create mode 100644 benchmarks/specfs_bench/data/spec/util/util.header create mode 100644 benchmarks/specfs_bench/env.toml.example create mode 100755 benchmarks/specfs_bench/install.sh create mode 100644 benchmarks/specfs_bench/requirements.txt create mode 100755 benchmarks/specfs_bench/run.sh create mode 100644 benchmarks/specfs_bench/src/evaluator.py create mode 100644 benchmarks/specfs_bench/src/genspec_prompt.md create mode 100644 benchmarks/specfs_bench/src/judge_prompt.md create mode 100644 benchmarks/specfs_bench/src/main.py create mode 100644 benchmarks/specfs_bench/tests/__init__.py diff --git a/benchmarks/specfs_bench/README.md b/benchmarks/specfs_bench/README.md new file mode 100644 index 00000000..f7efe61a --- /dev/null +++ b/benchmarks/specfs_bench/README.md @@ -0,0 +1,50 @@ +# SpecFS-Bench + +SpecFS-Bench evaluates LLM capability on **spec-to-code generation** for filesystem C functions. + +The pipeline contains two stages: + +1. **Generation**: For every `.spec` file under `data/spec`, ask the model to generate one corresponding C source file. +2. **Verification (LLM as Judge)**: Compare generated code against ground truth under `data/code` and output a simple score and diff summary. + +## Data Layout + +- `data/spec/**.spec`: formal function specifications and prompts. +- `data/code/**.c`: ground-truth implementation files (same relative path as spec, suffix changed to `.c`). + +Example mapping: + +- `data/spec/file/file_read.spec` +- `data/code/file/file_read.c` + +## Installation + +```bash +cd benchmarks/specfs_bench +./install.sh +``` + +## Configuration + +Create `env.toml` in this benchmark directory (or use workspace-level `benchmarks/env.toml`). + +You can copy from `env.toml.example` and fill your API credentials. + +## Run + +```bash +cd benchmarks/specfs_bench +./run.sh "gpt-4o" +# or use a separate judge model +./run.sh "openai/deepseek-chat" "gpt-4o" +``` + +## Outputs + +Each run writes into `outputs/specfsbench____judge___/`: + +- `generated/`: generated `.c` files preserving spec relative path. +- `generation_results.jsonl`: per-spec generation status. +- `judge_results.jsonl`: per-file judge results (score, verdict, differences). +- `summary.json`: aggregate metrics. + diff --git a/benchmarks/specfs_bench/data/spec/common.header b/benchmarks/specfs_bench/data/spec/common.header new file mode 100644 index 00000000..d15d05b4 --- /dev/null +++ b/benchmarks/specfs_bench/data/spec/common.header @@ -0,0 +1,67 @@ +string, stdio, stdlib, unistd, sys/syscall, assert + +#define FUSE_USE_VERSION 26 +#define FS_DATA ((struct fs_state *)fuse_get_context()->private_data) +#define LOCK_COUPLING + +#define FILE_MODE 1 +#define DIR_MODE 2 +#define CHR_MODE 3 +#define BLK_MODE 4 +#define SOCK_MODE 5 +#define FIFO_MODE 6 + +#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) + +typedef unsigned long long u64; +typedef struct entry { + char *name; + void *inum; + struct entry *next; +} entry; + +typedef struct indextb { + unsigned char *index[INDEXTB_NUM]; +} indextb; + +typedef struct dirtb { + struct entry *tb[DIRTB_NUM]; +} dirtb; + +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; + +typedef struct getattr_ret { + struct inode *inum; + unsigned mode; + unsigned size; + unsigned maj; + unsigned min; +} getattr_ret; + +typedef struct read_ret { + char *buf; + unsigned num; +} read_ret; + +extern struct inode *root_inum; + +struct fs_state { + FILE *logfile; +}; \ No newline at end of file diff --git a/benchmarks/specfs_bench/data/spec/file/file.header b/benchmarks/specfs_bench/data/spec/file/file.header new file mode 100644 index 00000000..74506099 --- /dev/null +++ b/benchmarks/specfs_bench/data/spec/file/file.header @@ -0,0 +1,5 @@ +common, util +void file_clear(struct inode *node, unsigned start, unsigned len); +void file_allocate(struct inode *node, unsigned offset, unsigned len); +void file_read(struct inode *node, unsigned offset, unsigned len, char *data); +void file_write(struct inode *node, unsigned offset, unsigned len, const char *data); 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.header b/benchmarks/specfs_bench/data/spec/inode/inode.header new file mode 100644 index 00000000..79bce7e7 --- /dev/null +++ b/benchmarks/specfs_bench/data/spec/inode/inode.header @@ -0,0 +1,7 @@ +common, util, file +int inode_insert(struct inode* cur, struct inode* inum, char* name); +struct inode* inode_delete(struct inode* inum, char* name); +unsigned inode_write(struct inode* node, const char* buffer, unsigned len, unsigned offset); +void inode_truncate(struct inode* node, unsigned size); +struct read_ret* inode_read(struct inode* node, unsigned len, unsigned offset); +struct inode *inode_find(struct inode *node, char *name); 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-util/interface-util.header b/benchmarks/specfs_bench/data/spec/interface-util/interface-util.header new file mode 100644 index 00000000..5580a3f2 --- /dev/null +++ b/benchmarks/specfs_bench/data/spec/interface-util/interface-util.header @@ -0,0 +1,8 @@ +inode, common, util +int check_file(struct inode *inum); +void check_unlock (struct inode* parent, struct inode* src, struct inode* dst); +int check_ins(struct inode *cur, char *name); +int check_dir(struct inode *inum); +int check_src_exist_dst_delete(struct inode *srcdir, struct inode *dstdir, char *srcname, char *dstname); +int check_del(struct inode *cur, char *name); +int check_open(struct inode *inum, unsigned mode); 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/interface/interface.header b/benchmarks/specfs_bench/data/spec/interface/interface.header new file mode 100644 index 00000000..bf95c577 --- /dev/null +++ b/benchmarks/specfs_bench/data/spec/interface/interface.header @@ -0,0 +1,10 @@ +common, util, inode, interface-util, path +struct inode *atomfs_open(char *path[], unsigned mode); +int atomfs_truncate(char* path[], unsigned offset); +int atomfs_rename(char* srcpath[], char* dstpath[], char* srcname, char* dstname); +char **atomfs_readdir(char *path[]); +struct read_ret* atomfs_read(char* path[], unsigned size, unsigned offset); +int atomfs_ins(char* path[], char* name, int mode, unsigned maj, unsigned min); +int atomfs_del(char* path[], char* name); +struct getattr_ret* atomfs_getattr(char* path[]); +int atomfs_write(char* path[], const char* buf, unsigned size, unsigned offset); 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/path/path.header b/benchmarks/specfs_bench/data/spec/path/path.header new file mode 100644 index 00000000..e3e228ed --- /dev/null +++ b/benchmarks/specfs_bench/data/spec/path/path.header @@ -0,0 +1,3 @@ +inode, common, util +struct inode* locate(struct inode* cur, char* path[]); +struct inode* locate_hold(struct inode *cur, char *path[]); 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/data/spec/util/util.header b/benchmarks/specfs_bench/data/spec/util/util.header new file mode 100644 index 00000000..a10d7ca9 --- /dev/null +++ b/benchmarks/specfs_bench/data/spec/util/util.header @@ -0,0 +1,24 @@ +stdlib, common, mcs +unsigned char* malloc_page(); +char** malloc_dir_content(unsigned size); +char* malloc_buffer(unsigned len); +struct read_ret* malloc_readret(); +void fill_dir(struct inode* inum, char** dircontent); +void free_dirs(char *dirname[]); +struct inode* malloc_inode(int mode, unsigned maj, unsigned min); +char** calculate(char* srcpath[], char* dstpath[]); +void free_path(char** path); +int getlen(char* path[]); +void lock(struct inode* inum); +void unlock2dir (struct inode* srcdir, struct inode* dstdir); +void unlock(struct inode* inum); +void dispose_inode(struct inode* inum); +char** malloc_path(unsigned len); +void free_readret(struct read_ret *p); +struct entry *malloc_entry(); +void split_dirs_file(const char *path, char *dirname[], char *filename); +void split_dirs(const char *path, char *dirname[]); +unsigned int hash_name(char* name); +char* malloc_string(const char* name); +void free_entry(struct entry* en); +struct getattr_ret* malloc_getattr_ret(struct inode* inum, unsigned mode, unsigned size, unsigned maj, unsigned min); 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 [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..aa4b08b9 --- /dev/null +++ b/benchmarks/specfs_bench/src/evaluator.py @@ -0,0 +1,84 @@ +"""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 SpecFsJudgeEvaluator: + """Evaluate generated C code against ground truth using an LLM judge.""" + + def __init__(self, model_name: str, system_prompt: str, user_template: str) -> None: + self.model_name = model_name + self.system_prompt = system_prompt + self.user_template = user_template + + def _build_prompt(self, spec_text: str, generated_code: str, ground_truth_code: str) -> str: + return ( + self.user_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, system_prompt=self.system_prompt, 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": , + "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..fc33b524 --- /dev/null +++ b/benchmarks/specfs_bench/src/main.py @@ -0,0 +1,304 @@ +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 SpecFsJudgeEvaluator + +GEN_DEFAULT_SYSTEM_PROMPT = 'You are an expert C systems programmer. Return robust, compilable C code only.' +JUDGE_DEFAULT_SYSTEM_PROMPT = 'You are a strict and fair C code reviewer and benchmark judge.' + + +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_user_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, GEN_DEFAULT_SYSTEM_PROMPT) + 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_user_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) + 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_user_template: str, +) -> list[dict[str, Any]]: + """Run LLM judge over generated code and ground truth code.""" + evaluator = SpecFsJudgeEvaluator( + model_name=judge_model_name, + system_prompt=JUDGE_DEFAULT_SYSTEM_PROMPT, + user_template=judge_user_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_user_template = load_prompt(generation_prompt_file) + judge_user_template = 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_user_template=generation_user_template, + ) + 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_user_template=judge_user_template, + ) + 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 From a9fadddda86d64a7ddabea3c2ddcb583f35aab4f Mon Sep 17 00:00:00 2001 From: HarryZ Date: Mon, 9 Mar 2026 11:22:13 +0800 Subject: [PATCH 2/5] minor update specfs evaluator --- benchmarks/specfs_bench/src/evaluator.py | 11 ++++----- benchmarks/specfs_bench/src/main.py | 29 ++++++++++++------------ 2 files changed, 19 insertions(+), 21 deletions(-) diff --git a/benchmarks/specfs_bench/src/evaluator.py b/benchmarks/specfs_bench/src/evaluator.py index aa4b08b9..53366899 100644 --- a/benchmarks/specfs_bench/src/evaluator.py +++ b/benchmarks/specfs_bench/src/evaluator.py @@ -21,17 +21,16 @@ class JudgeResult: raw_judge_response: str -class SpecFsJudgeEvaluator: +class JudgeEvaluator: """Evaluate generated C code against ground truth using an LLM judge.""" - def __init__(self, model_name: str, system_prompt: str, user_template: str) -> None: + def __init__(self, model_name: str, prompt_template: str) -> None: self.model_name = model_name - self.system_prompt = system_prompt - self.user_template = user_template + self.prompt_template = prompt_template def _build_prompt(self, spec_text: str, generated_code: str, ground_truth_code: str) -> str: return ( - self.user_template.replace('{{SPEC_CONTENT}}', spec_text) + self.prompt_template.replace('{{SPEC_CONTENT}}', spec_text) .replace('{{GENERATED_CODE}}', generated_code) .replace('{{GROUND_TRUTH_CODE}}', ground_truth_code) ) @@ -61,7 +60,7 @@ def _normalize_score(score: Any) -> float: 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, system_prompt=self.system_prompt, temperature=0.0, json_format=True) + 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) diff --git a/benchmarks/specfs_bench/src/main.py b/benchmarks/specfs_bench/src/main.py index fc33b524..c6a2c9c7 100644 --- a/benchmarks/specfs_bench/src/main.py +++ b/benchmarks/specfs_bench/src/main.py @@ -1,3 +1,5 @@ +"""Main entry point for the SpecFS benchmark.""" + from __future__ import annotations import argparse @@ -14,10 +16,7 @@ from sdk.logger import logger from sdk.utils import set_llm_endpoint_from_config -from evaluator import SpecFsJudgeEvaluator - -GEN_DEFAULT_SYSTEM_PROMPT = 'You are an expert C systems programmer. Return robust, compilable C code only.' -JUDGE_DEFAULT_SYSTEM_PROMPT = 'You are a strict and fair C code reviewer and benchmark judge.' +from evaluator import JudgeEvaluator def resolve_config_path(benchmark_root: Path) -> Path | None: @@ -68,13 +67,13 @@ def run_generation( spec_root: Path, output_dir: Path, model_name: str, - generation_user_template: 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, GEN_DEFAULT_SYSTEM_PROMPT) + executor = SimpleExecutor(model_name, "") results: list[dict[str, Any]] = [] for index, spec_path in enumerate(spec_files, start=1): @@ -83,7 +82,7 @@ def run_generation( output_code_path.parent.mkdir(parents=True, exist_ok=True) spec_text = read_text(spec_path) - prompt = generation_user_template.replace('{{SPEC_CONTENT}}', spec_text) + prompt = generation_prompt_template.replace('{{SPEC_CONTENT}}', spec_text) record: dict[str, Any] = { 'index': index, @@ -97,6 +96,7 @@ def run_generation( 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) @@ -111,13 +111,12 @@ def run_judging( generation_results: list[dict[str, Any]], code_root: Path, judge_model_name: str, - judge_user_template: str, + judge_prompt_template: str, ) -> list[dict[str, Any]]: """Run LLM judge over generated code and ground truth code.""" - evaluator = SpecFsJudgeEvaluator( + evaluator = JudgeEvaluator( model_name=judge_model_name, - system_prompt=JUDGE_DEFAULT_SYSTEM_PROMPT, - user_template=judge_user_template, + prompt_template=judge_prompt_template, ) judge_results: list[dict[str, Any]] = [] @@ -248,8 +247,8 @@ def main(args: argparse.Namespace) -> None: generation_prompt_file = current_dir / 'genspec_prompt.md' judge_prompt_file = current_dir / 'judge_prompt.md' - generation_user_template = load_prompt(generation_prompt_file) - judge_user_template = load_prompt(judge_prompt_file) + generation_prompt = load_prompt(generation_prompt_file) + judge_prompt = load_prompt(judge_prompt_file) logger.info('Discovered %s spec files.', len(spec_files)) @@ -258,7 +257,7 @@ def main(args: argparse.Namespace) -> None: spec_root=spec_root, output_dir=output_dir, model_name=args.model_name, - generation_user_template=generation_user_template, + generation_prompt_template=generation_prompt, ) write_jsonl(output_dir / 'generation_results.jsonl', generation_results) @@ -268,7 +267,7 @@ def main(args: argparse.Namespace) -> None: generation_results=generation_results, code_root=code_root, judge_model_name=args.judge_model_name, - judge_user_template=judge_user_template, + judge_prompt_template=judge_prompt, ) write_jsonl(output_dir / 'judge_results.jsonl', judge_results) From 7db07a0bef8f98a511a7d15f9dbba6b4880a941a Mon Sep 17 00:00:00 2001 From: yangjunqi Date: Wed, 18 Mar 2026 22:43:34 +0800 Subject: [PATCH 3/5] feat: add atomfs source code and update main script --- benchmarks/specfs_bench/data/code/.gitignore | 7 + benchmarks/specfs_bench/data/code/Makefile | 50 ++ .../specfs_bench/data/code/atomfs-fuse.c | 569 ++++++++++++++++++ benchmarks/specfs_bench/data/code/common.h | 77 +++ benchmarks/specfs_bench/data/code/file/file.h | 11 + .../data/code/file/file_allocate.c | 21 + .../specfs_bench/data/code/file/file_clear.c | 7 + .../specfs_bench/data/code/file/file_read.c | 22 + .../specfs_bench/data/code/file/file_write.c | 35 ++ .../specfs_bench/data/code/inode/inode.h | 14 + .../data/code/inode/inode_delete.c | 28 + .../specfs_bench/data/code/inode/inode_find.c | 15 + .../data/code/inode/inode_insert.c | 25 + .../specfs_bench/data/code/inode/inode_read.c | 22 + .../data/code/inode/inode_truncate.c | 13 + .../data/code/inode/inode_write.c | 34 ++ .../data/code/interface-util/check_del.c | 29 + .../data/code/interface-util/check_dir.c | 11 + .../data/code/interface-util/check_file.c | 14 + .../data/code/interface-util/check_ins.c | 24 + .../data/code/interface-util/check_open.c | 18 + .../check_src_exist_dst_delete.c | 68 +++ .../data/code/interface-util/check_unlock.c | 7 + .../data/code/interface-util/interface-util.h | 15 + .../data/code/interface/atomfs_del.c | 36 ++ .../data/code/interface/atomfs_getattr.c | 22 + .../data/code/interface/atomfs_ins.c | 37 ++ .../data/code/interface/atomfs_open.c | 18 + .../data/code/interface/atomfs_read.c | 17 + .../data/code/interface/atomfs_readdir.c | 41 ++ .../data/code/interface/atomfs_rename.c | 141 +++++ .../data/code/interface/atomfs_truncate.c | 32 + .../data/code/interface/atomfs_write.c | 34 ++ .../data/code/interface/interface.h | 19 + benchmarks/specfs_bench/data/code/mcs.c | 181 ++++++ benchmarks/specfs_bench/data/code/mcs.h | 61 ++ .../specfs_bench/data/code/path/locate.c | 34 ++ .../specfs_bench/data/code/path/locate_hold.c | 17 + benchmarks/specfs_bench/data/code/path/path.h | 10 + .../specfs_bench/data/code/util/calculate.c | 28 + .../data/code/util/dispose_inode.c | 40 ++ .../specfs_bench/data/code/util/fill_dir.c | 17 + .../specfs_bench/data/code/util/free_dirs.c | 9 + .../specfs_bench/data/code/util/free_entry.c | 6 + .../specfs_bench/data/code/util/free_path.c | 13 + .../data/code/util/free_readret.c | 6 + .../specfs_bench/data/code/util/getlen.c | 9 + .../specfs_bench/data/code/util/hash_name.c | 16 + benchmarks/specfs_bench/data/code/util/lock.c | 8 + .../data/code/util/malloc_buffer.c | 5 + .../data/code/util/malloc_dir_content.c | 5 + .../data/code/util/malloc_entry.c | 5 + .../data/code/util/malloc_getattr_ret.c | 21 + .../data/code/util/malloc_inode.c | 29 + .../specfs_bench/data/code/util/malloc_page.c | 5 + .../specfs_bench/data/code/util/malloc_path.c | 6 + .../data/code/util/malloc_readret.c | 10 + .../data/code/util/malloc_string.c | 8 + .../specfs_bench/data/code/util/split_dirs.c | 18 + .../data/code/util/split_dirs_file.c | 65 ++ .../specfs_bench/data/code/util/unlock.c | 8 + .../specfs_bench/data/code/util/unlock2dir.c | 10 + benchmarks/specfs_bench/data/code/util/util.h | 31 + 63 files changed, 2214 insertions(+) create mode 100644 benchmarks/specfs_bench/data/code/.gitignore create mode 100644 benchmarks/specfs_bench/data/code/Makefile create mode 100644 benchmarks/specfs_bench/data/code/atomfs-fuse.c create mode 100644 benchmarks/specfs_bench/data/code/common.h create mode 100644 benchmarks/specfs_bench/data/code/file/file.h create mode 100644 benchmarks/specfs_bench/data/code/file/file_allocate.c create mode 100644 benchmarks/specfs_bench/data/code/file/file_clear.c create mode 100644 benchmarks/specfs_bench/data/code/file/file_read.c create mode 100644 benchmarks/specfs_bench/data/code/file/file_write.c create mode 100644 benchmarks/specfs_bench/data/code/inode/inode.h create mode 100644 benchmarks/specfs_bench/data/code/inode/inode_delete.c create mode 100644 benchmarks/specfs_bench/data/code/inode/inode_find.c create mode 100644 benchmarks/specfs_bench/data/code/inode/inode_insert.c create mode 100644 benchmarks/specfs_bench/data/code/inode/inode_read.c create mode 100644 benchmarks/specfs_bench/data/code/inode/inode_truncate.c create mode 100644 benchmarks/specfs_bench/data/code/inode/inode_write.c create mode 100644 benchmarks/specfs_bench/data/code/interface-util/check_del.c create mode 100644 benchmarks/specfs_bench/data/code/interface-util/check_dir.c create mode 100644 benchmarks/specfs_bench/data/code/interface-util/check_file.c create mode 100644 benchmarks/specfs_bench/data/code/interface-util/check_ins.c create mode 100644 benchmarks/specfs_bench/data/code/interface-util/check_open.c create mode 100644 benchmarks/specfs_bench/data/code/interface-util/check_src_exist_dst_delete.c create mode 100644 benchmarks/specfs_bench/data/code/interface-util/check_unlock.c create mode 100644 benchmarks/specfs_bench/data/code/interface-util/interface-util.h create mode 100644 benchmarks/specfs_bench/data/code/interface/atomfs_del.c create mode 100644 benchmarks/specfs_bench/data/code/interface/atomfs_getattr.c create mode 100644 benchmarks/specfs_bench/data/code/interface/atomfs_ins.c create mode 100644 benchmarks/specfs_bench/data/code/interface/atomfs_open.c create mode 100644 benchmarks/specfs_bench/data/code/interface/atomfs_read.c create mode 100644 benchmarks/specfs_bench/data/code/interface/atomfs_readdir.c create mode 100644 benchmarks/specfs_bench/data/code/interface/atomfs_rename.c create mode 100644 benchmarks/specfs_bench/data/code/interface/atomfs_truncate.c create mode 100644 benchmarks/specfs_bench/data/code/interface/atomfs_write.c create mode 100644 benchmarks/specfs_bench/data/code/interface/interface.h create mode 100644 benchmarks/specfs_bench/data/code/mcs.c create mode 100644 benchmarks/specfs_bench/data/code/mcs.h create mode 100644 benchmarks/specfs_bench/data/code/path/locate.c create mode 100644 benchmarks/specfs_bench/data/code/path/locate_hold.c create mode 100644 benchmarks/specfs_bench/data/code/path/path.h create mode 100644 benchmarks/specfs_bench/data/code/util/calculate.c create mode 100644 benchmarks/specfs_bench/data/code/util/dispose_inode.c create mode 100644 benchmarks/specfs_bench/data/code/util/fill_dir.c create mode 100644 benchmarks/specfs_bench/data/code/util/free_dirs.c create mode 100644 benchmarks/specfs_bench/data/code/util/free_entry.c create mode 100644 benchmarks/specfs_bench/data/code/util/free_path.c create mode 100644 benchmarks/specfs_bench/data/code/util/free_readret.c create mode 100644 benchmarks/specfs_bench/data/code/util/getlen.c create mode 100644 benchmarks/specfs_bench/data/code/util/hash_name.c create mode 100644 benchmarks/specfs_bench/data/code/util/lock.c create mode 100644 benchmarks/specfs_bench/data/code/util/malloc_buffer.c create mode 100644 benchmarks/specfs_bench/data/code/util/malloc_dir_content.c create mode 100644 benchmarks/specfs_bench/data/code/util/malloc_entry.c create mode 100644 benchmarks/specfs_bench/data/code/util/malloc_getattr_ret.c create mode 100644 benchmarks/specfs_bench/data/code/util/malloc_inode.c create mode 100644 benchmarks/specfs_bench/data/code/util/malloc_page.c create mode 100644 benchmarks/specfs_bench/data/code/util/malloc_path.c create mode 100644 benchmarks/specfs_bench/data/code/util/malloc_readret.c create mode 100644 benchmarks/specfs_bench/data/code/util/malloc_string.c create mode 100644 benchmarks/specfs_bench/data/code/util/split_dirs.c create mode 100644 benchmarks/specfs_bench/data/code/util/split_dirs_file.c create mode 100644 benchmarks/specfs_bench/data/code/util/unlock.c create mode 100644 benchmarks/specfs_bench/data/code/util/unlock2dir.c create mode 100644 benchmarks/specfs_bench/data/code/util/util.h diff --git a/benchmarks/specfs_bench/data/code/.gitignore b/benchmarks/specfs_bench/data/code/.gitignore new file mode 100644 index 00000000..3628f8ff --- /dev/null +++ b/benchmarks/specfs_bench/data/code/.gitignore @@ -0,0 +1,7 @@ +atomfs-fuse + +compile_commands.json + +*.o + +.cache \ No newline at end of file diff --git a/benchmarks/specfs_bench/data/code/Makefile b/benchmarks/specfs_bench/data/code/Makefile new file mode 100644 index 00000000..1cf8901a --- /dev/null +++ b/benchmarks/specfs_bench/data/code/Makefile @@ -0,0 +1,50 @@ +CC := gcc +CFLAGS := $(shell pkg-config fuse --cflags) -pthread -Wall -O2 -I. -Iutil -Ifile -Iinode -Iinterface -Iinterface-util -Ipath +LDFLAGS := $(shell pkg-config fuse --libs) + +DEBUG_CFLAGS := -g -DDEBUG + +TARGET := atomfs-fuse +DEBUG_TARGET := $(TARGET)-debug + +SOURCES := $(shell find . -name '*.c') +OBJS := $(SOURCES:.c=.o) +DEBUG_OBJS := $(SOURCES:.c=-debug.o) + +RM := rm -f + +.PHONY: all clean run debug + +all: $(TARGET) + +$(TARGET): $(OBJS) + @echo "==> Linking Release: $@" + $(CC) -o $@ $^ $(LDFLAGS) + +$(DEBUG_TARGET): $(DEBUG_OBJS) + @echo "==> Linking Debug: $@" + $(CC) -o $@ $^ $(LDFLAGS) + +%.o: %.c + @echo "Compiling (Release) $< -> $@" + $(CC) $(CFLAGS) -c -o $@ $< + +%-debug.o: %.c + @echo "Compiling (Debug) $< -> $@" + $(CC) $(CFLAGS) $(DEBUG_CFLAGS) -c -o $@ $< + +run: $(TARGET) + @echo "==> Running filesystem..." + -mkdir -p ~/atomfs > /dev/null 2>&1 + ./$(TARGET) -n /dev/pmem0 ~/atomfs + +debug: $(DEBUG_TARGET) + @echo "==> Preparing to debug..." + -mkdir -p /tmp/fs > /dev/null 2>&1 + -sudo umount /tmp/fs >/dev/null 2>&1 + echo "r -n /dev/pmem0 /tmp/fs" > /tmp/parms + exec gdb -x /tmp/parms ./$(DEBUG_TARGET) + +clean: + @echo "==> Cleaning up project..." + $(RM) $(TARGET) $(DEBUG_TARGET) $(OBJS) $(DEBUG_OBJS) /tmp/parms \ No newline at end of file diff --git a/benchmarks/specfs_bench/data/code/atomfs-fuse.c b/benchmarks/specfs_bench/data/code/atomfs-fuse.c new file mode 100644 index 00000000..decab2fa --- /dev/null +++ b/benchmarks/specfs_bench/data/code/atomfs-fuse.c @@ -0,0 +1,569 @@ +/* * Copyright (c) 2020 Institution of Parallel and Distributed System, Shanghai Jiao Tong University + * AtomFS is licensed under the Mulan PSL v1. + * You can use this software according to the terms and conditions of the Mulan PSL v1. + * You may obtain a copy of Mulan PSL v1 at: + * http://license.coscl.org.cn/MulanPSL + * THIS SOFTWARE IS PROVIDED ON AN "AS IS" BASIS, WITHOUT WARRANTIES OF ANY KIND, EITHER EXPRESS OR + * IMPLIED, INCLUDING BUT NOT LIMITED TO NON-INFRINGEMENT, MERCHANTABILITY OR FIT FOR A PARTICULAR + * PURPOSE. + * See the Mulan PSL v1 for more details. + */ + +#define _GNU_SOURCE +#include "common.h" +#include "util.h" +#include "interface.h" +#include +#include +#include +#include +#include +#include +#include + +char *device; +char *mpoint; +bool mkfs; +struct inode *root_inum; + +#define log_pmsg(fmt, ...) \ + log_msg("(%s:%d) " fmt, __func__, __LINE__, ##__VA_ARGS__) +FILE *logfile; +FILE *log_open() +{ + return NULL; +} +void log_msg(const char *format, ...) +{ +} + +int fs_mknod(const char *path, mode_t mode, dev_t dev) +{ + char *dirname[MAX_PATH_LEN]; + char filename[MAX_FILE_LEN]; + unsigned res; + + log_msg("\nfs_mknod(path=\"%s\", mode=0%3o, dev=%lld)\n", path, mode, + dev); + + memset(dirname, 0, MAX_PATH_LEN * sizeof(char *)); + memset(filename, 0, MAX_FILE_LEN); + split_dirs_file(path, dirname, filename); + if (strlen(filename) == 0) { + free_dirs(dirname); + return -1; + } + if (S_ISREG(mode)) + res = atomfs_ins(dirname, filename, FILE_MODE, 0, 0); + else if (S_ISSOCK(mode)) + res = atomfs_ins(dirname, filename, SOCK_MODE, 0, 0); + else if (S_ISFIFO(mode)) + res = atomfs_ins(dirname, filename, FIFO_MODE, 0, 0); + else if (S_ISCHR(mode)) + res = atomfs_ins(dirname, filename, CHR_MODE, major(dev), + minor(dev)); + else + res = atomfs_ins(dirname, filename, BLK_MODE, major(dev), + minor(dev)); + free_dirs(dirname); + return res; +} + +/** Create a directory */ +int fs_mkdir(const char *path, mode_t mode) +{ + char *dirname[MAX_PATH_LEN]; + char filename[MAX_FILE_LEN]; + unsigned res; + + log_msg("\nfs_mkdir(path=\"%s\", mode=0%3o)\n", path, mode); + + memset(dirname, 0, MAX_PATH_LEN * sizeof(char *)); + memset(filename, 0, MAX_FILE_LEN); + split_dirs_file(path, dirname, filename); + if (strlen(filename) == 0) { + free_dirs(dirname); + return -1; + } + res = atomfs_ins(dirname, filename, DIR_MODE, 0, 0); + free_dirs(dirname); + return res; +} + +/** Remove a file */ +int fs_unlink(const char *path) +{ + char *dirname[MAX_PATH_LEN]; + char filename[MAX_FILE_LEN]; + unsigned res; + + log_msg("fs_unlink(path=\"%s\")\n", path); + + if (strcmp(path, "/") == 0) { + return -1; + } + memset(dirname, 0, MAX_PATH_LEN * sizeof(char *)); + memset(filename, 0, MAX_FILE_LEN); + split_dirs_file(path, dirname, filename); + if (strlen(filename) == 0) { + free_dirs(dirname); + return -1; + } + res = atomfs_del(dirname, filename); + free_dirs(dirname); + return res; +} + +/** Remove a directory */ +int fs_rmdir(const char *path) +{ + char *dirname[MAX_PATH_LEN]; + char filename[MAX_FILE_LEN]; + unsigned res; + + log_pmsg("(path=\"%s\")\n", path); + if (strcmp(path, "/") == 0) { + return -1; + } + memset(dirname, 0, MAX_PATH_LEN * sizeof(char *)); + memset(filename, 0, MAX_FILE_LEN); + split_dirs_file(path, dirname, filename); + if (strlen(filename) == 0) { + free_dirs(dirname); + return -1; + } + res = atomfs_del(dirname, filename); + free_dirs(dirname); + return res; +} + +/** Rename a file */ +int fs_rename(const char *path, const char *newpath) +{ + char *srcdir[MAX_PATH_LEN]; + char *dstdir[MAX_PATH_LEN]; + char srcname[MAX_FILE_LEN]; + char dstname[MAX_FILE_LEN]; + int res; + + log_pmsg("(fpath=\"%s\", newpath=\"%s\")\n", path, newpath); + memset(srcdir, 0, MAX_PATH_LEN * sizeof(char *)); + memset(srcname, 0, MAX_FILE_LEN); + memset(dstdir, 0, MAX_PATH_LEN * sizeof(char *)); + memset(dstname, 0, MAX_FILE_LEN); + split_dirs_file(path, srcdir, srcname); + split_dirs_file(newpath, dstdir, dstname); + if ((strlen(srcname) == 0) || (strlen(dstname) == 0)) { + free_dirs(srcdir); + free_dirs(dstdir); + return -1; + } + res = atomfs_rename(srcdir, dstdir, srcname, dstname); + free_dirs(srcdir); + free_dirs(dstdir); + return res; +} + +/** Change the size of a file */ +int fs_truncate(const char *path, off_t newsize) +{ + char *dirname[MAX_PATH_LEN]; + unsigned res; + + if (newsize & 0xffffffff00000000) + return -1; + log_pmsg("(path=\"%s\", newsize=%lld)\n", path, newsize); + memset(dirname, 0, MAX_PATH_LEN * sizeof(char *)); + split_dirs(path, dirname); + res = atomfs_truncate(dirname, newsize); + + free_dirs(dirname); + return res; +} + +/** Files are accessed using path + * Open is not used + * */ +int fs_open(const char *path, struct fuse_file_info *fi) +{ + char *dirname[MAX_PATH_LEN]; + struct inode *ret; + + log_pmsg("(path\"%s\", fi=0x%08x)\n", path, fi); + memset(dirname, 0, MAX_PATH_LEN * sizeof(char *)); + split_dirs(path, dirname); + ret = atomfs_open(dirname, FILE_MODE); + if (ret == NULL) { + free_dirs(dirname); + return -1; + } + free_dirs(dirname); + return 0; +} + +int fs_read(const char *path, char *buf, size_t size, off_t offset, + struct fuse_file_info *fi) +{ + char *dirname[MAX_PATH_LEN]; + struct read_ret *res; + unsigned temp; + + if ((size > MAX_FILE_SIZE) || ((size_t)offset > MAX_FILE_SIZE)) { + return -1; + } + log_pmsg("(path=\"%s\", buf=0x%08x, size=%d, offset=%lld, fi=0x%08x)\n", + path, buf, size, offset, fi); + memset(dirname, 0, MAX_PATH_LEN * sizeof(char *)); + split_dirs(path, dirname); + res = atomfs_read(dirname, size, offset); + + free_dirs(dirname); + + if (res == NULL) + return -1; + if (res->num) + memcpy(buf, res->buf, res->num); + temp = res->num; + free_readret(res); + return temp; +} + +int fs_write(const char *path, const char *buf, size_t size, off_t offset, + struct fuse_file_info *fi) +{ + char *dirname[MAX_PATH_LEN]; + int res; + + if ((size > MAX_FILE_SIZE) || ((size_t)offset > MAX_FILE_SIZE)) { + return -1; + } + log_pmsg("(path=\"%s\", buf=0x%08x, size=%d, offset=%lld, fi=0x%08x)\n", + path, buf, size, offset, fi); + memset(dirname, 0, MAX_PATH_LEN * sizeof(char *)); + split_dirs(path, dirname); + res = atomfs_write(dirname, buf, size, offset); + free_dirs(dirname); + return res; +} + +int fs_opendir(const char *path, struct fuse_file_info *fi) +{ + char *dirname[MAX_PATH_LEN]; + struct inode *ret; + + log_pmsg("fs_opendir(path=\"%s\", fi=0x%08x)\n", path, fi); + memset(dirname, 0, MAX_PATH_LEN * sizeof(char *)); + split_dirs(path, dirname); + ret = atomfs_open(dirname, DIR_MODE); + if (ret == NULL) { + free_dirs(dirname); + return -1; + } + free_dirs(dirname); + return 0; +} + +int fs_readdir(const char *path, void *buf, fuse_fill_dir_t filler, + off_t offset, struct fuse_file_info *fi) +{ + char *dirname[MAX_PATH_LEN]; + char **dircontent; + unsigned i = 0; + + log_pmsg( + "(path=\"%s\", buf=0x%08x, filler=0x%08x, offset=%lld, fi=0x%08x)\n", + path, buf, filler, offset, fi); + + memset(dirname, 0, MAX_PATH_LEN * sizeof(char *)); + split_dirs(path, dirname); + dircontent = atomfs_readdir(dirname); + free_dirs(dirname); + if (dircontent == NULL) { + return -1; + } + + filler(buf, ".", NULL, 0); + filler(buf, "..", NULL, 0); + for (; dircontent[i]; ++i) { + if (filler(buf, dircontent[i], NULL, 0) != 0) { + for (; dircontent[i]; ++i) + free(dircontent[i]); + free(dircontent); + return -ENOMEM; + } + free(dircontent[i]); + } + free(dircontent); + return 0; +} + +int fs_getattr(const char *path, struct stat *statbuf) +{ + char *dirname[MAX_PATH_LEN]; + struct getattr_ret *attr; + + log_pmsg("fs_getattr(path=\"%s\", statbuf=0x%08x)\n", path, statbuf); + memset(dirname, 0, MAX_PATH_LEN * sizeof(char *)); + split_dirs(path, dirname); + attr = atomfs_getattr(dirname); + if (!attr) { + free_dirs(dirname); + return -ENOENT; + } + statbuf->st_dev = 0; + statbuf->st_ino = (u64)(attr->inum); + statbuf->st_uid = 0; + statbuf->st_gid = 0; + + statbuf->st_rdev = makedev(attr->maj, attr->min); + if (attr->mode == FILE_MODE) { + statbuf->st_mode = 0777 | S_IFREG; + statbuf->st_size = attr->size; + } else if (attr->mode == DIR_MODE) { + statbuf->st_mode = 0777 | S_IFDIR; + statbuf->st_size = attr->size; + } else { + if (attr->mode == SOCK_MODE) + statbuf->st_mode = 0777 | S_IFSOCK; + else if (attr->mode == FIFO_MODE) + statbuf->st_mode = 0777 | S_IFIFO; + else if (attr->mode == CHR_MODE) + statbuf->st_mode = 0777 | S_IFCHR; + else + statbuf->st_mode = 0777 | S_IFBLK; + statbuf->st_size = 0; + } + statbuf->st_blksize = PAGE_SIZE; + statbuf->st_blocks = 1; + statbuf->st_atim.tv_sec = 0; + statbuf->st_atim.tv_nsec = 0; + statbuf->st_mtim.tv_sec = 0; + statbuf->st_mtim.tv_nsec = 0; + statbuf->st_ctim.tv_sec = 0; + statbuf->st_ctim.tv_nsec = 0; + + free(attr); + + free_dirs(dirname); + return 0; +} + +int fs_statfs(const char *path, struct statvfs *statv) +{ + log_msg("statfs\n"); + statv->f_bsize = PAGE_SIZE; /* Filesystem block size */ + statv->f_frsize = PAGE_SIZE; /* Fragment size */ + statv->f_blocks = 0; /* Size of fs in f_frsize units */ + statv->f_bfree = 0; /* Number of free blocks */ + statv->f_bavail = 0; /* Number of free blocks for + unprivileged users */ + statv->f_files = 1; /* Number of inodes */ + statv->f_ffree = 10000; /* Number of free inodes */ + statv->f_favail = 10000; /* Number of free inodes for + unprivileged users */ + statv->f_fsid = 0x50F5; /* Filesystem ID */ + statv->f_flag = 0; /* Mount flags */ + statv->f_namemax = 39; /* Maximum filename length */ + return 0; +} + +int fs_readlink(const char *path, char *link, size_t size) +{ + log_msg("read_link\n"); + return 0; +} + +void *fs_init(struct fuse_conn_info *conn) +{ + log_msg("\nfs_init()\n"); + return FS_DATA; +} + +void fs_destroy(void *userdata) +{ + log_msg("fs_destroy(userdata=0x%08x)\n", userdata); + return; +} + +int fs_symlink(const char *path, const char *link) +{ + log_msg("sym_link\n"); + return -ENOSYS; +} + +int fs_link(const char *path, const char *newpath) +{ + log_msg("link\n"); + return -ENOSYS; +} + +int fs_chmod(const char *path, mode_t mode) +{ + log_msg("chmod\n"); + return 0; +} + +int fs_chown(const char *path, uid_t uid, gid_t gid) +{ + log_msg("chown\n"); + return 0; +} + +int fs_utimens(const char *path, const struct timespec tv[2]) +{ + log_msg("utime\n"); + return 0; +} + +int fs_flush(const char *path, struct fuse_file_info *fi) +{ + log_msg("flush\n"); + return 0; +} + +int fs_release(const char *path, struct fuse_file_info *fi) +{ + log_msg("release\n"); + return 0; +} + +int fs_releasedir(const char *path, struct fuse_file_info *fi) +{ + log_msg("releasedir\n"); + return 0; +} + +int fs_access(const char *path, int mask) +{ + log_msg("access\n"); + return 0; +} + +int fs_fsyncdir(const char *path, int datasync, struct fuse_file_info *fi) +{ + log_msg("(path=\"%s\", datasync=%d, fi=0x%08x)\n", path, datasync, fi); + return 0; +} + +int fs_fsync(const char *path, int datasync, struct fuse_file_info *fi) +{ + log_msg("(path=\"%s\", datasync=%d, fi=0x%08x)\n", path, datasync, fi); + return 0; +} + +struct fuse_operations fs_oper = { + .getattr = fs_getattr, + .readlink = fs_readlink, + + .getdir = NULL, + .mknod = fs_mknod, + .mkdir = fs_mkdir, + .unlink = fs_unlink, + .rmdir = fs_rmdir, + .symlink = fs_symlink, + .rename = fs_rename, + .link = fs_link, + .chmod = fs_chmod, + .chown = fs_chown, + .truncate = fs_truncate, + .utimens = fs_utimens, + .open = fs_open, + .read = fs_read, + .write = fs_write, + .statfs = fs_statfs, + .flush = fs_flush, + .release = fs_release, + .fsync = fs_fsync, + .opendir = fs_opendir, + .readdir = fs_readdir, + .releasedir = fs_releasedir, + .fsyncdir = fs_fsyncdir, + .init = fs_init, + .destroy = fs_destroy, + .access = fs_access, + .ftruncate = NULL, +}; + +void parse_opts(int argc, char *argv[]) +{ + int opt; + bool init = false; + while ((opt = getopt(argc, argv, "n")) != -1) { + switch (opt) { + case 'n': + init = true; + break; + default: + fprintf(stderr, "Usage: %s [-n] device mountPoint\n", + argv[0]); + fprintf(stderr, " option: -n, make a new fs\n"); + abort(); + } + } + if (optind + 1 >= argc) { + fprintf(stderr, "Expect device and mount point!\n"); + abort(); + } + + device = argv[optind]; + mpoint = argv[optind + 1]; + mkfs = init; +} + +int main(int argc, char *argv[]) +{ + int fuse_stat; + struct fs_state *fs_data = NULL; + if ((getuid() == 0) || (geteuid() == 0)) { + fprintf(stderr, + "Running AtomFS as root opens unnacceptable security holes\n"); + return 1; + } + + // See which version of fuse we're running + fprintf(stderr, "Fuse library version %d.%d\n", FUSE_MAJOR_VERSION, + FUSE_MINOR_VERSION); + + parse_opts(argc, argv); + + printf("atomfs: mount device '%s' at '%s'\n", device, mpoint); + + fs_data = malloc(sizeof(struct fs_state)); + if (fs_data == NULL) { + perror("main calloc"); + abort(); + } + + fs_data->logfile = log_open(); + + argc--; + argv[1] = argv[2]; + argv[2] = argv[3]; + argc--; + argv[1] = argv[2]; + + //added by atomfs + root_inum = malloc_inode(DIR_MODE, 0, 0); + struct fuse_args args = FUSE_ARGS_INIT(0, NULL); + fuse_opt_add_arg(&args, argv[0]); +#ifdef DEBUG + fuse_opt_add_arg(&args, "-d"); + fuse_opt_add_arg(&args, "-odebug"); +#endif + fuse_opt_add_arg(&args, "-f"); + fuse_opt_add_arg(&args, argv[1]); + + fuse_opt_add_arg(&args, "-oallow_root"); + + printf("args.argc= %d\n", args.argc); + int i; + for (i = 0; i < args.argc; ++i) + printf("args.argv[%d] = %s\n", i, args.argv[i]); + + // turn over control to fuse + fprintf(stderr, "about to call fuse_main\n"); + fuse_stat = fuse_main(args.argc, args.argv, &fs_oper, fs_data); + fprintf(stderr, "fuse_main returned %d\n", fuse_stat); + + return fuse_stat; +} diff --git a/benchmarks/specfs_bench/data/code/common.h b/benchmarks/specfs_bench/data/code/common.h new file mode 100644 index 00000000..ece385e5 --- /dev/null +++ b/benchmarks/specfs_bench/data/code/common.h @@ -0,0 +1,77 @@ +#ifndef _COMMON_H +#define _COMMON_H + +#include +#include +#include +#include +#include +#include + + +#define FUSE_USE_VERSION 26 +#define FS_DATA ((struct fs_state *)fuse_get_context()->private_data) +#define LOCK_COUPLING + +#define FILE_MODE 1 +#define DIR_MODE 2 +#define CHR_MODE 3 +#define BLK_MODE 4 +#define SOCK_MODE 5 +#define FIFO_MODE 6 + +#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) + +typedef unsigned long long u64; +typedef struct entry { + char *name; + void *inum; + struct entry *next; +} entry; + +typedef struct indextb { + unsigned char *index[INDEXTB_NUM]; +} indextb; + +typedef struct dirtb { + struct entry *tb[DIRTB_NUM]; +} dirtb; + +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; + +typedef struct getattr_ret { + struct inode *inum; + unsigned mode; + unsigned size; + unsigned maj; + unsigned min; +} getattr_ret; + +typedef struct read_ret { + char *buf; + unsigned num; +} read_ret; + +extern struct inode *root_inum; + +struct fs_state { + FILE *logfile; +}; +#endif // _COMMON_H \ No newline at end of file diff --git a/benchmarks/specfs_bench/data/code/file/file.h b/benchmarks/specfs_bench/data/code/file/file.h new file mode 100644 index 00000000..f2acdf7e --- /dev/null +++ b/benchmarks/specfs_bench/data/code/file/file.h @@ -0,0 +1,11 @@ +#ifndef _FILE_H +#define _FILE_H + +#include "common.h" +#include "util.h" + +void file_clear(struct inode *node, unsigned start, unsigned len); +void file_allocate(struct inode *node, unsigned offset, unsigned len); +void file_read(struct inode *node, unsigned offset, unsigned len, char *data); +void file_write(struct inode *node, unsigned offset, unsigned len, const char *data); +#endif // _FILE_H \ No newline at end of file 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.h b/benchmarks/specfs_bench/data/code/inode/inode.h new file mode 100644 index 00000000..446ec8f4 --- /dev/null +++ b/benchmarks/specfs_bench/data/code/inode/inode.h @@ -0,0 +1,14 @@ +#ifndef _INODE_H +#define _INODE_H + +#include "common.h" +#include "util.h" +#include "file.h" + +int inode_insert(struct inode* cur, struct inode* inum, char* name); +struct inode* inode_delete(struct inode* inum, char* name); +unsigned inode_write(struct inode* node, const char* buffer, unsigned len, unsigned offset); +void inode_truncate(struct inode* node, unsigned size); +struct read_ret* inode_read(struct inode* node, unsigned len, unsigned offset); +struct inode *inode_find(struct inode *node, char *name); +#endif // _INODE_H \ 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-util/interface-util.h b/benchmarks/specfs_bench/data/code/interface-util/interface-util.h new file mode 100644 index 00000000..405b949c --- /dev/null +++ b/benchmarks/specfs_bench/data/code/interface-util/interface-util.h @@ -0,0 +1,15 @@ +#ifndef _INTERFACE_UTIL_H +#define _INTERFACE_UTIL_H + +#include "inode.h" +#include "common.h" +#include "util.h" + +int check_file(struct inode *inum); +void check_unlock (struct inode* parent, struct inode* src, struct inode* dst); +int check_ins(struct inode *cur, char *name); +int check_dir(struct inode *inum); +int check_src_exist_dst_delete(struct inode *srcdir, struct inode *dstdir, char *srcname, char *dstname); +int check_del(struct inode *cur, char *name); +int check_open(struct inode *inum, unsigned mode); +#endif // _INTERFACE_UTIL_H \ 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/interface/interface.h b/benchmarks/specfs_bench/data/code/interface/interface.h new file mode 100644 index 00000000..16ecbd0f --- /dev/null +++ b/benchmarks/specfs_bench/data/code/interface/interface.h @@ -0,0 +1,19 @@ +#ifndef _INTERFACE_H +#define _INTERFACE_H + +#include "common.h" +#include "util.h" +#include "inode.h" +#include "interface-util.h" +#include "path.h" + +struct inode *atomfs_open(char *path[], unsigned mode); +int atomfs_truncate(char* path[], unsigned offset); +int atomfs_rename(char* srcpath[], char* dstpath[], char* srcname, char* dstname); +char **atomfs_readdir(char *path[]); +struct read_ret* atomfs_read(char* path[], unsigned size, unsigned offset); +int atomfs_ins(char* path[], char* name, int mode, unsigned maj, unsigned min); +int atomfs_del(char* path[], char* name); +struct getattr_ret* atomfs_getattr(char* path[]); +int atomfs_write(char* path[], const char* buf, unsigned size, unsigned offset); +#endif // _INTERFACE_H \ No newline at end of file diff --git a/benchmarks/specfs_bench/data/code/mcs.c b/benchmarks/specfs_bench/data/code/mcs.c new file mode 100644 index 00000000..c507961e --- /dev/null +++ b/benchmarks/specfs_bench/data/code/mcs.c @@ -0,0 +1,181 @@ +/* + * The MIT License (MIT) + * + * Copyright (c) 2016 Hugo Guiroux + * UPMC, 2010-2011, Jean-Pierre Lozi + * Gaël Thomas + * Florian David + * Julia Lawall + * Gilles Muller + * + * Permission is hereby granted, free of charge, to any person obtaining a copy + * of his software and associated documentation files (the "Software"), to deal + * in the Software without restriction, including without limitation the rights + * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell + * copies of the Software, and to permit persons to whom the Software is + * furnished to do so, subject to the following conditions: + * + * The above copyright notice and this permission notice shall be included in + * all copies or substantial portions of the Software. + * + * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR + * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, + * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE + * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER + * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, + * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE + * SOFTWARE. + * + * + * John M. Mellor-Crummey and Michael L. Scott. 1991. + * Algorithms for scalable synchronization on shared-memory multiprocessors. + * ACM Trans. Comput. Syst. 9, 1 (February 1991). + * + * Lock design summary: + * The MCS lock is one of the most known multicore locks. + * Its main goal is to avoid all threads spinning on the same memory address as + * it induces contention due to the cache coherency protocol. + * The lock is organized as a FIFO list: this ensures total fairness. + * Each thread as its own context, which is a node that the thread will put into + * the linked list (representing the list of threads waiting for the lock) when + * it tries to grab the lock. + * The lock is a linked-list composed of a pointer to the tail of the list. + * - On lock: the thread does an atomic xchg to put itself to the end of the + * linked list and get the previous tail of the list. + * If there was no other thread waiting, then the thread has the lock. + * Otherwise, the thread spins on a memory address contained in its context. + * - On unlock: if there is any thread, we just wake the next thread on the + * waiting list. Otherwise we set the tail of the queue to NULL. + */ + +/* + * [Module Name] MCS + * [Rely] None + */ + +#include +#include +#include +#include +#include +#include +#include +#include +#include "mcs.h" + +#define CPU_PAUSE() asm volatile("pause\n") +#define COMPILER_BARRIER() asm volatile("" : : : "memory") + +static inline void *xchg_64(void *ptr, void *x) +{ + __asm__ __volatile__("xchgq %0,%1" + : "=r"((unsigned long long)x) + : "m"(*(volatile long long *)ptr), + "0"((unsigned long long)x) + : "memory"); + + return x; +} + +static inline void *alloc_cache_align(size_t n) +{ + void *res = 0; + if ((MEMALIGN(&res, L_CACHE_LINE_SIZE, cache_align(n)) < 0) || !res) { + fprintf(stderr, "MEMALIGN(%llu, %llu)", (unsigned long long)n, + (unsigned long long)cache_align(n)); + exit(-1); + } + return res; +} + +static inline void waiting_policy_sleep(volatile int *var) +{ + while (!(*var)) { + CPU_PAUSE(); + } +} + +static inline void waiting_policy_wake(volatile int *var) +{ + *var = UNLOCKED; + //assert(old == 0); +} + +mcs_mutex_t *mcs_mutex_create() +{ + mcs_mutex_t *impl = + (mcs_mutex_t *)alloc_cache_align(sizeof(mcs_mutex_t)); + impl->tail = 0; + return impl; +} + +static int __mcs_mutex_lock(mcs_mutex_t *impl, mcs_node_t *me) +{ + mcs_node_t *tail; + + //assert(me != NULL); + + me->next = LOCKED; + me->spin = 0; + + // The atomic instruction is needed when two threads try to put themselves + // at the tail of the list at the same time + tail = xchg_64((void *)&impl->tail, (void *)me); + + /* No one there? */ + if (!tail) { + return 0; + } + + /* Someone there, need to link in */ + tail->next = me; + COMPILER_BARRIER(); + + //waiting_policy_sleep(&me->spin); + while (!me->spin) { + CPU_PAUSE(); + } + + return 0; +} + +int mcs_mutex_lock(mcs_mutex_t *impl, mcs_node_t *me) +{ + int ret = __mcs_mutex_lock(impl, me); + //assert(ret == 0); + //DEBUG("[%d] Lock acquired posix=%p\n", cur_thread_id, &impl->posix_lock); + return ret; +} + +static void __mcs_mutex_unlock(mcs_mutex_t *impl, mcs_node_t *me) +{ + /* No successor yet? */ + if (!me->next) { + // The atomic instruction is needed if a thread between the previous if + // and now has enqueued itself at the tail + if (__sync_val_compare_and_swap(&impl->tail, me, 0) == me) + return; + + /* Wait for successor to appear */ + while (!me->next) { + CPU_PAUSE(); + } + } + + /* Unlock next one */ + //waiting_policy_wake(&me->next->spin); + me->next->spin = UNLOCKED; +} + +void mcs_mutex_unlock(mcs_mutex_t *impl, mcs_node_t *me) +{ + __mcs_mutex_unlock(impl, me); +} + +int mcs_mutex_destroy(mcs_mutex_t *lock) +{ + free(lock); + lock = NULL; + + return 0; +} diff --git a/benchmarks/specfs_bench/data/code/mcs.h b/benchmarks/specfs_bench/data/code/mcs.h new file mode 100644 index 00000000..38adc724 --- /dev/null +++ b/benchmarks/specfs_bench/data/code/mcs.h @@ -0,0 +1,61 @@ +/* + * The MIT License (MIT) + * + * Copyright (c) 2016 Hugo Guiroux + * + * Permission is hereby granted, free of charge, to any person obtaining a copy + * of his software and associated documentation files (the "Software"), to deal + * in the Software without restriction, including without limitation the rights + * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell + * copies of the Software, and to permit persons to whom the Software is + * furnished to do so, subject to the following conditions: + * + * The above copyright notice and this permission notice shall be included in + * all copies or substantial portions of the Software. + * + * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR + * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, + * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE + * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER + * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, + * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE + * SOFTWARE. + */ +#ifndef __MCS_H__ +#define __MCS_H__ + +#define _GNU_SOURCE + +#define NUMA_NODES 2 +#define CPU_NUMBER 32 +#define L_CACHE_LINE_SIZE 128 +#define LOCKED 0 +#define UNLOCKED 1 +#define SPINNING_THRESHOLD 2700LL + +#define r_align(n, r) (((n) + (r) - 1) & -(r)) +#define cache_align(n) r_align(n, L_CACHE_LINE_SIZE) +#define pad_to_cache_line(n) (cache_align(n) - (n)) +#define MEMALIGN(ptr, alignment, size) \ + posix_memalign((void **)(ptr), (alignment), (size)) + +typedef struct mcs_node { + struct mcs_node *volatile next; + char __pad[pad_to_cache_line(sizeof(struct mcs_node *))]; + volatile int spin __attribute__((aligned(L_CACHE_LINE_SIZE))); +} mcs_node_t __attribute__((aligned(L_CACHE_LINE_SIZE))); + +typedef struct mcs_mutex { + struct mcs_node *volatile tail + __attribute__((aligned(L_CACHE_LINE_SIZE))); +} mcs_mutex_t __attribute__((aligned(L_CACHE_LINE_SIZE))); + +mcs_mutex_t *mcs_mutex_create(); +int mcs_mutex_lock(mcs_mutex_t *impl, mcs_node_t *me); +void mcs_mutex_unlock(mcs_mutex_t *impl, mcs_node_t *me); +int mcs_mutex_destroy(mcs_mutex_t *lock); + +typedef mcs_mutex_t lock_mutex_t; +typedef mcs_node_t lock_context_t; + +#endif // __MCS_H__ 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/path/path.h b/benchmarks/specfs_bench/data/code/path/path.h new file mode 100644 index 00000000..cf232207 --- /dev/null +++ b/benchmarks/specfs_bench/data/code/path/path.h @@ -0,0 +1,10 @@ +#ifndef _PATH_H +#define _PATH_H + +#include "inode.h" +#include "common.h" +#include "util.h" + +struct inode* locate(struct inode* cur, char* path[]); +struct inode* locate_hold(struct inode *cur, char *path[]); +#endif // _PATH_H \ 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/code/util/util.h b/benchmarks/specfs_bench/data/code/util/util.h new file mode 100644 index 00000000..00d505b7 --- /dev/null +++ b/benchmarks/specfs_bench/data/code/util/util.h @@ -0,0 +1,31 @@ +#ifndef _UTIL_H +#define _UTIL_H + +#include +#include "common.h" +#include "mcs.h" + +unsigned char* malloc_page(); +char** malloc_dir_content(unsigned size); +char* malloc_buffer(unsigned len); +struct read_ret* malloc_readret(); +void fill_dir(struct inode* inum, char** dircontent); +void free_dirs(char *dirname[]); +struct inode* malloc_inode(int mode, unsigned maj, unsigned min); +char** calculate(char* srcpath[], char* dstpath[]); +void free_path(char** path); +int getlen(char* path[]); +void lock(struct inode* inum); +void unlock2dir (struct inode* srcdir, struct inode* dstdir); +void unlock(struct inode* inum); +void dispose_inode(struct inode* inum); +char** malloc_path(unsigned len); +void free_readret(struct read_ret *p); +struct entry *malloc_entry(); +void split_dirs_file(const char *path, char *dirname[], char *filename); +void split_dirs(const char *path, char *dirname[]); +unsigned int hash_name(char* name); +char* malloc_string(const char* name); +void free_entry(struct entry* en); +struct getattr_ret* malloc_getattr_ret(struct inode* inum, unsigned mode, unsigned size, unsigned maj, unsigned min); +#endif // _UTIL_H \ No newline at end of file From ac607972c31aae3b9919662e6636715984a52f7a Mon Sep 17 00:00:00 2001 From: HarryZ Date: Mon, 20 Apr 2026 17:09:30 +0800 Subject: [PATCH 4/5] feat: remove unrelated source code for simplicity --- benchmarks/specfs_bench/data/code/.gitignore | 7 - benchmarks/specfs_bench/data/code/Makefile | 50 -- .../specfs_bench/data/code/atomfs-fuse.c | 569 ------------------ benchmarks/specfs_bench/data/code/common.h | 77 --- benchmarks/specfs_bench/data/code/file/file.h | 11 - .../specfs_bench/data/code/inode/inode.h | 14 - .../data/code/interface-util/interface-util.h | 15 - .../data/code/interface/interface.h | 19 - benchmarks/specfs_bench/data/code/mcs.c | 181 ------ benchmarks/specfs_bench/data/code/mcs.h | 61 -- benchmarks/specfs_bench/data/code/path/path.h | 10 - benchmarks/specfs_bench/data/code/util/util.h | 31 - .../specfs_bench/data/spec/common.header | 67 --- .../specfs_bench/data/spec/file/file.header | 5 - .../specfs_bench/data/spec/inode/inode.header | 7 - .../spec/interface-util/interface-util.header | 8 - .../data/spec/interface/interface.header | 10 - .../specfs_bench/data/spec/path/path.header | 3 - .../specfs_bench/data/spec/util/util.header | 24 - 19 files changed, 1169 deletions(-) delete mode 100644 benchmarks/specfs_bench/data/code/.gitignore delete mode 100644 benchmarks/specfs_bench/data/code/Makefile delete mode 100644 benchmarks/specfs_bench/data/code/atomfs-fuse.c delete mode 100644 benchmarks/specfs_bench/data/code/common.h delete mode 100644 benchmarks/specfs_bench/data/code/file/file.h delete mode 100644 benchmarks/specfs_bench/data/code/inode/inode.h delete mode 100644 benchmarks/specfs_bench/data/code/interface-util/interface-util.h delete mode 100644 benchmarks/specfs_bench/data/code/interface/interface.h delete mode 100644 benchmarks/specfs_bench/data/code/mcs.c delete mode 100644 benchmarks/specfs_bench/data/code/mcs.h delete mode 100644 benchmarks/specfs_bench/data/code/path/path.h delete mode 100644 benchmarks/specfs_bench/data/code/util/util.h delete mode 100644 benchmarks/specfs_bench/data/spec/common.header delete mode 100644 benchmarks/specfs_bench/data/spec/file/file.header delete mode 100644 benchmarks/specfs_bench/data/spec/inode/inode.header delete mode 100644 benchmarks/specfs_bench/data/spec/interface-util/interface-util.header delete mode 100644 benchmarks/specfs_bench/data/spec/interface/interface.header delete mode 100644 benchmarks/specfs_bench/data/spec/path/path.header delete mode 100644 benchmarks/specfs_bench/data/spec/util/util.header diff --git a/benchmarks/specfs_bench/data/code/.gitignore b/benchmarks/specfs_bench/data/code/.gitignore deleted file mode 100644 index 3628f8ff..00000000 --- a/benchmarks/specfs_bench/data/code/.gitignore +++ /dev/null @@ -1,7 +0,0 @@ -atomfs-fuse - -compile_commands.json - -*.o - -.cache \ No newline at end of file diff --git a/benchmarks/specfs_bench/data/code/Makefile b/benchmarks/specfs_bench/data/code/Makefile deleted file mode 100644 index 1cf8901a..00000000 --- a/benchmarks/specfs_bench/data/code/Makefile +++ /dev/null @@ -1,50 +0,0 @@ -CC := gcc -CFLAGS := $(shell pkg-config fuse --cflags) -pthread -Wall -O2 -I. -Iutil -Ifile -Iinode -Iinterface -Iinterface-util -Ipath -LDFLAGS := $(shell pkg-config fuse --libs) - -DEBUG_CFLAGS := -g -DDEBUG - -TARGET := atomfs-fuse -DEBUG_TARGET := $(TARGET)-debug - -SOURCES := $(shell find . -name '*.c') -OBJS := $(SOURCES:.c=.o) -DEBUG_OBJS := $(SOURCES:.c=-debug.o) - -RM := rm -f - -.PHONY: all clean run debug - -all: $(TARGET) - -$(TARGET): $(OBJS) - @echo "==> Linking Release: $@" - $(CC) -o $@ $^ $(LDFLAGS) - -$(DEBUG_TARGET): $(DEBUG_OBJS) - @echo "==> Linking Debug: $@" - $(CC) -o $@ $^ $(LDFLAGS) - -%.o: %.c - @echo "Compiling (Release) $< -> $@" - $(CC) $(CFLAGS) -c -o $@ $< - -%-debug.o: %.c - @echo "Compiling (Debug) $< -> $@" - $(CC) $(CFLAGS) $(DEBUG_CFLAGS) -c -o $@ $< - -run: $(TARGET) - @echo "==> Running filesystem..." - -mkdir -p ~/atomfs > /dev/null 2>&1 - ./$(TARGET) -n /dev/pmem0 ~/atomfs - -debug: $(DEBUG_TARGET) - @echo "==> Preparing to debug..." - -mkdir -p /tmp/fs > /dev/null 2>&1 - -sudo umount /tmp/fs >/dev/null 2>&1 - echo "r -n /dev/pmem0 /tmp/fs" > /tmp/parms - exec gdb -x /tmp/parms ./$(DEBUG_TARGET) - -clean: - @echo "==> Cleaning up project..." - $(RM) $(TARGET) $(DEBUG_TARGET) $(OBJS) $(DEBUG_OBJS) /tmp/parms \ No newline at end of file diff --git a/benchmarks/specfs_bench/data/code/atomfs-fuse.c b/benchmarks/specfs_bench/data/code/atomfs-fuse.c deleted file mode 100644 index decab2fa..00000000 --- a/benchmarks/specfs_bench/data/code/atomfs-fuse.c +++ /dev/null @@ -1,569 +0,0 @@ -/* * Copyright (c) 2020 Institution of Parallel and Distributed System, Shanghai Jiao Tong University - * AtomFS is licensed under the Mulan PSL v1. - * You can use this software according to the terms and conditions of the Mulan PSL v1. - * You may obtain a copy of Mulan PSL v1 at: - * http://license.coscl.org.cn/MulanPSL - * THIS SOFTWARE IS PROVIDED ON AN "AS IS" BASIS, WITHOUT WARRANTIES OF ANY KIND, EITHER EXPRESS OR - * IMPLIED, INCLUDING BUT NOT LIMITED TO NON-INFRINGEMENT, MERCHANTABILITY OR FIT FOR A PARTICULAR - * PURPOSE. - * See the Mulan PSL v1 for more details. - */ - -#define _GNU_SOURCE -#include "common.h" -#include "util.h" -#include "interface.h" -#include -#include -#include -#include -#include -#include -#include - -char *device; -char *mpoint; -bool mkfs; -struct inode *root_inum; - -#define log_pmsg(fmt, ...) \ - log_msg("(%s:%d) " fmt, __func__, __LINE__, ##__VA_ARGS__) -FILE *logfile; -FILE *log_open() -{ - return NULL; -} -void log_msg(const char *format, ...) -{ -} - -int fs_mknod(const char *path, mode_t mode, dev_t dev) -{ - char *dirname[MAX_PATH_LEN]; - char filename[MAX_FILE_LEN]; - unsigned res; - - log_msg("\nfs_mknod(path=\"%s\", mode=0%3o, dev=%lld)\n", path, mode, - dev); - - memset(dirname, 0, MAX_PATH_LEN * sizeof(char *)); - memset(filename, 0, MAX_FILE_LEN); - split_dirs_file(path, dirname, filename); - if (strlen(filename) == 0) { - free_dirs(dirname); - return -1; - } - if (S_ISREG(mode)) - res = atomfs_ins(dirname, filename, FILE_MODE, 0, 0); - else if (S_ISSOCK(mode)) - res = atomfs_ins(dirname, filename, SOCK_MODE, 0, 0); - else if (S_ISFIFO(mode)) - res = atomfs_ins(dirname, filename, FIFO_MODE, 0, 0); - else if (S_ISCHR(mode)) - res = atomfs_ins(dirname, filename, CHR_MODE, major(dev), - minor(dev)); - else - res = atomfs_ins(dirname, filename, BLK_MODE, major(dev), - minor(dev)); - free_dirs(dirname); - return res; -} - -/** Create a directory */ -int fs_mkdir(const char *path, mode_t mode) -{ - char *dirname[MAX_PATH_LEN]; - char filename[MAX_FILE_LEN]; - unsigned res; - - log_msg("\nfs_mkdir(path=\"%s\", mode=0%3o)\n", path, mode); - - memset(dirname, 0, MAX_PATH_LEN * sizeof(char *)); - memset(filename, 0, MAX_FILE_LEN); - split_dirs_file(path, dirname, filename); - if (strlen(filename) == 0) { - free_dirs(dirname); - return -1; - } - res = atomfs_ins(dirname, filename, DIR_MODE, 0, 0); - free_dirs(dirname); - return res; -} - -/** Remove a file */ -int fs_unlink(const char *path) -{ - char *dirname[MAX_PATH_LEN]; - char filename[MAX_FILE_LEN]; - unsigned res; - - log_msg("fs_unlink(path=\"%s\")\n", path); - - if (strcmp(path, "/") == 0) { - return -1; - } - memset(dirname, 0, MAX_PATH_LEN * sizeof(char *)); - memset(filename, 0, MAX_FILE_LEN); - split_dirs_file(path, dirname, filename); - if (strlen(filename) == 0) { - free_dirs(dirname); - return -1; - } - res = atomfs_del(dirname, filename); - free_dirs(dirname); - return res; -} - -/** Remove a directory */ -int fs_rmdir(const char *path) -{ - char *dirname[MAX_PATH_LEN]; - char filename[MAX_FILE_LEN]; - unsigned res; - - log_pmsg("(path=\"%s\")\n", path); - if (strcmp(path, "/") == 0) { - return -1; - } - memset(dirname, 0, MAX_PATH_LEN * sizeof(char *)); - memset(filename, 0, MAX_FILE_LEN); - split_dirs_file(path, dirname, filename); - if (strlen(filename) == 0) { - free_dirs(dirname); - return -1; - } - res = atomfs_del(dirname, filename); - free_dirs(dirname); - return res; -} - -/** Rename a file */ -int fs_rename(const char *path, const char *newpath) -{ - char *srcdir[MAX_PATH_LEN]; - char *dstdir[MAX_PATH_LEN]; - char srcname[MAX_FILE_LEN]; - char dstname[MAX_FILE_LEN]; - int res; - - log_pmsg("(fpath=\"%s\", newpath=\"%s\")\n", path, newpath); - memset(srcdir, 0, MAX_PATH_LEN * sizeof(char *)); - memset(srcname, 0, MAX_FILE_LEN); - memset(dstdir, 0, MAX_PATH_LEN * sizeof(char *)); - memset(dstname, 0, MAX_FILE_LEN); - split_dirs_file(path, srcdir, srcname); - split_dirs_file(newpath, dstdir, dstname); - if ((strlen(srcname) == 0) || (strlen(dstname) == 0)) { - free_dirs(srcdir); - free_dirs(dstdir); - return -1; - } - res = atomfs_rename(srcdir, dstdir, srcname, dstname); - free_dirs(srcdir); - free_dirs(dstdir); - return res; -} - -/** Change the size of a file */ -int fs_truncate(const char *path, off_t newsize) -{ - char *dirname[MAX_PATH_LEN]; - unsigned res; - - if (newsize & 0xffffffff00000000) - return -1; - log_pmsg("(path=\"%s\", newsize=%lld)\n", path, newsize); - memset(dirname, 0, MAX_PATH_LEN * sizeof(char *)); - split_dirs(path, dirname); - res = atomfs_truncate(dirname, newsize); - - free_dirs(dirname); - return res; -} - -/** Files are accessed using path - * Open is not used - * */ -int fs_open(const char *path, struct fuse_file_info *fi) -{ - char *dirname[MAX_PATH_LEN]; - struct inode *ret; - - log_pmsg("(path\"%s\", fi=0x%08x)\n", path, fi); - memset(dirname, 0, MAX_PATH_LEN * sizeof(char *)); - split_dirs(path, dirname); - ret = atomfs_open(dirname, FILE_MODE); - if (ret == NULL) { - free_dirs(dirname); - return -1; - } - free_dirs(dirname); - return 0; -} - -int fs_read(const char *path, char *buf, size_t size, off_t offset, - struct fuse_file_info *fi) -{ - char *dirname[MAX_PATH_LEN]; - struct read_ret *res; - unsigned temp; - - if ((size > MAX_FILE_SIZE) || ((size_t)offset > MAX_FILE_SIZE)) { - return -1; - } - log_pmsg("(path=\"%s\", buf=0x%08x, size=%d, offset=%lld, fi=0x%08x)\n", - path, buf, size, offset, fi); - memset(dirname, 0, MAX_PATH_LEN * sizeof(char *)); - split_dirs(path, dirname); - res = atomfs_read(dirname, size, offset); - - free_dirs(dirname); - - if (res == NULL) - return -1; - if (res->num) - memcpy(buf, res->buf, res->num); - temp = res->num; - free_readret(res); - return temp; -} - -int fs_write(const char *path, const char *buf, size_t size, off_t offset, - struct fuse_file_info *fi) -{ - char *dirname[MAX_PATH_LEN]; - int res; - - if ((size > MAX_FILE_SIZE) || ((size_t)offset > MAX_FILE_SIZE)) { - return -1; - } - log_pmsg("(path=\"%s\", buf=0x%08x, size=%d, offset=%lld, fi=0x%08x)\n", - path, buf, size, offset, fi); - memset(dirname, 0, MAX_PATH_LEN * sizeof(char *)); - split_dirs(path, dirname); - res = atomfs_write(dirname, buf, size, offset); - free_dirs(dirname); - return res; -} - -int fs_opendir(const char *path, struct fuse_file_info *fi) -{ - char *dirname[MAX_PATH_LEN]; - struct inode *ret; - - log_pmsg("fs_opendir(path=\"%s\", fi=0x%08x)\n", path, fi); - memset(dirname, 0, MAX_PATH_LEN * sizeof(char *)); - split_dirs(path, dirname); - ret = atomfs_open(dirname, DIR_MODE); - if (ret == NULL) { - free_dirs(dirname); - return -1; - } - free_dirs(dirname); - return 0; -} - -int fs_readdir(const char *path, void *buf, fuse_fill_dir_t filler, - off_t offset, struct fuse_file_info *fi) -{ - char *dirname[MAX_PATH_LEN]; - char **dircontent; - unsigned i = 0; - - log_pmsg( - "(path=\"%s\", buf=0x%08x, filler=0x%08x, offset=%lld, fi=0x%08x)\n", - path, buf, filler, offset, fi); - - memset(dirname, 0, MAX_PATH_LEN * sizeof(char *)); - split_dirs(path, dirname); - dircontent = atomfs_readdir(dirname); - free_dirs(dirname); - if (dircontent == NULL) { - return -1; - } - - filler(buf, ".", NULL, 0); - filler(buf, "..", NULL, 0); - for (; dircontent[i]; ++i) { - if (filler(buf, dircontent[i], NULL, 0) != 0) { - for (; dircontent[i]; ++i) - free(dircontent[i]); - free(dircontent); - return -ENOMEM; - } - free(dircontent[i]); - } - free(dircontent); - return 0; -} - -int fs_getattr(const char *path, struct stat *statbuf) -{ - char *dirname[MAX_PATH_LEN]; - struct getattr_ret *attr; - - log_pmsg("fs_getattr(path=\"%s\", statbuf=0x%08x)\n", path, statbuf); - memset(dirname, 0, MAX_PATH_LEN * sizeof(char *)); - split_dirs(path, dirname); - attr = atomfs_getattr(dirname); - if (!attr) { - free_dirs(dirname); - return -ENOENT; - } - statbuf->st_dev = 0; - statbuf->st_ino = (u64)(attr->inum); - statbuf->st_uid = 0; - statbuf->st_gid = 0; - - statbuf->st_rdev = makedev(attr->maj, attr->min); - if (attr->mode == FILE_MODE) { - statbuf->st_mode = 0777 | S_IFREG; - statbuf->st_size = attr->size; - } else if (attr->mode == DIR_MODE) { - statbuf->st_mode = 0777 | S_IFDIR; - statbuf->st_size = attr->size; - } else { - if (attr->mode == SOCK_MODE) - statbuf->st_mode = 0777 | S_IFSOCK; - else if (attr->mode == FIFO_MODE) - statbuf->st_mode = 0777 | S_IFIFO; - else if (attr->mode == CHR_MODE) - statbuf->st_mode = 0777 | S_IFCHR; - else - statbuf->st_mode = 0777 | S_IFBLK; - statbuf->st_size = 0; - } - statbuf->st_blksize = PAGE_SIZE; - statbuf->st_blocks = 1; - statbuf->st_atim.tv_sec = 0; - statbuf->st_atim.tv_nsec = 0; - statbuf->st_mtim.tv_sec = 0; - statbuf->st_mtim.tv_nsec = 0; - statbuf->st_ctim.tv_sec = 0; - statbuf->st_ctim.tv_nsec = 0; - - free(attr); - - free_dirs(dirname); - return 0; -} - -int fs_statfs(const char *path, struct statvfs *statv) -{ - log_msg("statfs\n"); - statv->f_bsize = PAGE_SIZE; /* Filesystem block size */ - statv->f_frsize = PAGE_SIZE; /* Fragment size */ - statv->f_blocks = 0; /* Size of fs in f_frsize units */ - statv->f_bfree = 0; /* Number of free blocks */ - statv->f_bavail = 0; /* Number of free blocks for - unprivileged users */ - statv->f_files = 1; /* Number of inodes */ - statv->f_ffree = 10000; /* Number of free inodes */ - statv->f_favail = 10000; /* Number of free inodes for - unprivileged users */ - statv->f_fsid = 0x50F5; /* Filesystem ID */ - statv->f_flag = 0; /* Mount flags */ - statv->f_namemax = 39; /* Maximum filename length */ - return 0; -} - -int fs_readlink(const char *path, char *link, size_t size) -{ - log_msg("read_link\n"); - return 0; -} - -void *fs_init(struct fuse_conn_info *conn) -{ - log_msg("\nfs_init()\n"); - return FS_DATA; -} - -void fs_destroy(void *userdata) -{ - log_msg("fs_destroy(userdata=0x%08x)\n", userdata); - return; -} - -int fs_symlink(const char *path, const char *link) -{ - log_msg("sym_link\n"); - return -ENOSYS; -} - -int fs_link(const char *path, const char *newpath) -{ - log_msg("link\n"); - return -ENOSYS; -} - -int fs_chmod(const char *path, mode_t mode) -{ - log_msg("chmod\n"); - return 0; -} - -int fs_chown(const char *path, uid_t uid, gid_t gid) -{ - log_msg("chown\n"); - return 0; -} - -int fs_utimens(const char *path, const struct timespec tv[2]) -{ - log_msg("utime\n"); - return 0; -} - -int fs_flush(const char *path, struct fuse_file_info *fi) -{ - log_msg("flush\n"); - return 0; -} - -int fs_release(const char *path, struct fuse_file_info *fi) -{ - log_msg("release\n"); - return 0; -} - -int fs_releasedir(const char *path, struct fuse_file_info *fi) -{ - log_msg("releasedir\n"); - return 0; -} - -int fs_access(const char *path, int mask) -{ - log_msg("access\n"); - return 0; -} - -int fs_fsyncdir(const char *path, int datasync, struct fuse_file_info *fi) -{ - log_msg("(path=\"%s\", datasync=%d, fi=0x%08x)\n", path, datasync, fi); - return 0; -} - -int fs_fsync(const char *path, int datasync, struct fuse_file_info *fi) -{ - log_msg("(path=\"%s\", datasync=%d, fi=0x%08x)\n", path, datasync, fi); - return 0; -} - -struct fuse_operations fs_oper = { - .getattr = fs_getattr, - .readlink = fs_readlink, - - .getdir = NULL, - .mknod = fs_mknod, - .mkdir = fs_mkdir, - .unlink = fs_unlink, - .rmdir = fs_rmdir, - .symlink = fs_symlink, - .rename = fs_rename, - .link = fs_link, - .chmod = fs_chmod, - .chown = fs_chown, - .truncate = fs_truncate, - .utimens = fs_utimens, - .open = fs_open, - .read = fs_read, - .write = fs_write, - .statfs = fs_statfs, - .flush = fs_flush, - .release = fs_release, - .fsync = fs_fsync, - .opendir = fs_opendir, - .readdir = fs_readdir, - .releasedir = fs_releasedir, - .fsyncdir = fs_fsyncdir, - .init = fs_init, - .destroy = fs_destroy, - .access = fs_access, - .ftruncate = NULL, -}; - -void parse_opts(int argc, char *argv[]) -{ - int opt; - bool init = false; - while ((opt = getopt(argc, argv, "n")) != -1) { - switch (opt) { - case 'n': - init = true; - break; - default: - fprintf(stderr, "Usage: %s [-n] device mountPoint\n", - argv[0]); - fprintf(stderr, " option: -n, make a new fs\n"); - abort(); - } - } - if (optind + 1 >= argc) { - fprintf(stderr, "Expect device and mount point!\n"); - abort(); - } - - device = argv[optind]; - mpoint = argv[optind + 1]; - mkfs = init; -} - -int main(int argc, char *argv[]) -{ - int fuse_stat; - struct fs_state *fs_data = NULL; - if ((getuid() == 0) || (geteuid() == 0)) { - fprintf(stderr, - "Running AtomFS as root opens unnacceptable security holes\n"); - return 1; - } - - // See which version of fuse we're running - fprintf(stderr, "Fuse library version %d.%d\n", FUSE_MAJOR_VERSION, - FUSE_MINOR_VERSION); - - parse_opts(argc, argv); - - printf("atomfs: mount device '%s' at '%s'\n", device, mpoint); - - fs_data = malloc(sizeof(struct fs_state)); - if (fs_data == NULL) { - perror("main calloc"); - abort(); - } - - fs_data->logfile = log_open(); - - argc--; - argv[1] = argv[2]; - argv[2] = argv[3]; - argc--; - argv[1] = argv[2]; - - //added by atomfs - root_inum = malloc_inode(DIR_MODE, 0, 0); - struct fuse_args args = FUSE_ARGS_INIT(0, NULL); - fuse_opt_add_arg(&args, argv[0]); -#ifdef DEBUG - fuse_opt_add_arg(&args, "-d"); - fuse_opt_add_arg(&args, "-odebug"); -#endif - fuse_opt_add_arg(&args, "-f"); - fuse_opt_add_arg(&args, argv[1]); - - fuse_opt_add_arg(&args, "-oallow_root"); - - printf("args.argc= %d\n", args.argc); - int i; - for (i = 0; i < args.argc; ++i) - printf("args.argv[%d] = %s\n", i, args.argv[i]); - - // turn over control to fuse - fprintf(stderr, "about to call fuse_main\n"); - fuse_stat = fuse_main(args.argc, args.argv, &fs_oper, fs_data); - fprintf(stderr, "fuse_main returned %d\n", fuse_stat); - - return fuse_stat; -} diff --git a/benchmarks/specfs_bench/data/code/common.h b/benchmarks/specfs_bench/data/code/common.h deleted file mode 100644 index ece385e5..00000000 --- a/benchmarks/specfs_bench/data/code/common.h +++ /dev/null @@ -1,77 +0,0 @@ -#ifndef _COMMON_H -#define _COMMON_H - -#include -#include -#include -#include -#include -#include - - -#define FUSE_USE_VERSION 26 -#define FS_DATA ((struct fs_state *)fuse_get_context()->private_data) -#define LOCK_COUPLING - -#define FILE_MODE 1 -#define DIR_MODE 2 -#define CHR_MODE 3 -#define BLK_MODE 4 -#define SOCK_MODE 5 -#define FIFO_MODE 6 - -#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) - -typedef unsigned long long u64; -typedef struct entry { - char *name; - void *inum; - struct entry *next; -} entry; - -typedef struct indextb { - unsigned char *index[INDEXTB_NUM]; -} indextb; - -typedef struct dirtb { - struct entry *tb[DIRTB_NUM]; -} dirtb; - -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; - -typedef struct getattr_ret { - struct inode *inum; - unsigned mode; - unsigned size; - unsigned maj; - unsigned min; -} getattr_ret; - -typedef struct read_ret { - char *buf; - unsigned num; -} read_ret; - -extern struct inode *root_inum; - -struct fs_state { - FILE *logfile; -}; -#endif // _COMMON_H \ No newline at end of file diff --git a/benchmarks/specfs_bench/data/code/file/file.h b/benchmarks/specfs_bench/data/code/file/file.h deleted file mode 100644 index f2acdf7e..00000000 --- a/benchmarks/specfs_bench/data/code/file/file.h +++ /dev/null @@ -1,11 +0,0 @@ -#ifndef _FILE_H -#define _FILE_H - -#include "common.h" -#include "util.h" - -void file_clear(struct inode *node, unsigned start, unsigned len); -void file_allocate(struct inode *node, unsigned offset, unsigned len); -void file_read(struct inode *node, unsigned offset, unsigned len, char *data); -void file_write(struct inode *node, unsigned offset, unsigned len, const char *data); -#endif // _FILE_H \ No newline at end of file diff --git a/benchmarks/specfs_bench/data/code/inode/inode.h b/benchmarks/specfs_bench/data/code/inode/inode.h deleted file mode 100644 index 446ec8f4..00000000 --- a/benchmarks/specfs_bench/data/code/inode/inode.h +++ /dev/null @@ -1,14 +0,0 @@ -#ifndef _INODE_H -#define _INODE_H - -#include "common.h" -#include "util.h" -#include "file.h" - -int inode_insert(struct inode* cur, struct inode* inum, char* name); -struct inode* inode_delete(struct inode* inum, char* name); -unsigned inode_write(struct inode* node, const char* buffer, unsigned len, unsigned offset); -void inode_truncate(struct inode* node, unsigned size); -struct read_ret* inode_read(struct inode* node, unsigned len, unsigned offset); -struct inode *inode_find(struct inode *node, char *name); -#endif // _INODE_H \ No newline at end of file diff --git a/benchmarks/specfs_bench/data/code/interface-util/interface-util.h b/benchmarks/specfs_bench/data/code/interface-util/interface-util.h deleted file mode 100644 index 405b949c..00000000 --- a/benchmarks/specfs_bench/data/code/interface-util/interface-util.h +++ /dev/null @@ -1,15 +0,0 @@ -#ifndef _INTERFACE_UTIL_H -#define _INTERFACE_UTIL_H - -#include "inode.h" -#include "common.h" -#include "util.h" - -int check_file(struct inode *inum); -void check_unlock (struct inode* parent, struct inode* src, struct inode* dst); -int check_ins(struct inode *cur, char *name); -int check_dir(struct inode *inum); -int check_src_exist_dst_delete(struct inode *srcdir, struct inode *dstdir, char *srcname, char *dstname); -int check_del(struct inode *cur, char *name); -int check_open(struct inode *inum, unsigned mode); -#endif // _INTERFACE_UTIL_H \ No newline at end of file diff --git a/benchmarks/specfs_bench/data/code/interface/interface.h b/benchmarks/specfs_bench/data/code/interface/interface.h deleted file mode 100644 index 16ecbd0f..00000000 --- a/benchmarks/specfs_bench/data/code/interface/interface.h +++ /dev/null @@ -1,19 +0,0 @@ -#ifndef _INTERFACE_H -#define _INTERFACE_H - -#include "common.h" -#include "util.h" -#include "inode.h" -#include "interface-util.h" -#include "path.h" - -struct inode *atomfs_open(char *path[], unsigned mode); -int atomfs_truncate(char* path[], unsigned offset); -int atomfs_rename(char* srcpath[], char* dstpath[], char* srcname, char* dstname); -char **atomfs_readdir(char *path[]); -struct read_ret* atomfs_read(char* path[], unsigned size, unsigned offset); -int atomfs_ins(char* path[], char* name, int mode, unsigned maj, unsigned min); -int atomfs_del(char* path[], char* name); -struct getattr_ret* atomfs_getattr(char* path[]); -int atomfs_write(char* path[], const char* buf, unsigned size, unsigned offset); -#endif // _INTERFACE_H \ No newline at end of file diff --git a/benchmarks/specfs_bench/data/code/mcs.c b/benchmarks/specfs_bench/data/code/mcs.c deleted file mode 100644 index c507961e..00000000 --- a/benchmarks/specfs_bench/data/code/mcs.c +++ /dev/null @@ -1,181 +0,0 @@ -/* - * The MIT License (MIT) - * - * Copyright (c) 2016 Hugo Guiroux - * UPMC, 2010-2011, Jean-Pierre Lozi - * Gaël Thomas - * Florian David - * Julia Lawall - * Gilles Muller - * - * Permission is hereby granted, free of charge, to any person obtaining a copy - * of his software and associated documentation files (the "Software"), to deal - * in the Software without restriction, including without limitation the rights - * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell - * copies of the Software, and to permit persons to whom the Software is - * furnished to do so, subject to the following conditions: - * - * The above copyright notice and this permission notice shall be included in - * all copies or substantial portions of the Software. - * - * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR - * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, - * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE - * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER - * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, - * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE - * SOFTWARE. - * - * - * John M. Mellor-Crummey and Michael L. Scott. 1991. - * Algorithms for scalable synchronization on shared-memory multiprocessors. - * ACM Trans. Comput. Syst. 9, 1 (February 1991). - * - * Lock design summary: - * The MCS lock is one of the most known multicore locks. - * Its main goal is to avoid all threads spinning on the same memory address as - * it induces contention due to the cache coherency protocol. - * The lock is organized as a FIFO list: this ensures total fairness. - * Each thread as its own context, which is a node that the thread will put into - * the linked list (representing the list of threads waiting for the lock) when - * it tries to grab the lock. - * The lock is a linked-list composed of a pointer to the tail of the list. - * - On lock: the thread does an atomic xchg to put itself to the end of the - * linked list and get the previous tail of the list. - * If there was no other thread waiting, then the thread has the lock. - * Otherwise, the thread spins on a memory address contained in its context. - * - On unlock: if there is any thread, we just wake the next thread on the - * waiting list. Otherwise we set the tail of the queue to NULL. - */ - -/* - * [Module Name] MCS - * [Rely] None - */ - -#include -#include -#include -#include -#include -#include -#include -#include -#include "mcs.h" - -#define CPU_PAUSE() asm volatile("pause\n") -#define COMPILER_BARRIER() asm volatile("" : : : "memory") - -static inline void *xchg_64(void *ptr, void *x) -{ - __asm__ __volatile__("xchgq %0,%1" - : "=r"((unsigned long long)x) - : "m"(*(volatile long long *)ptr), - "0"((unsigned long long)x) - : "memory"); - - return x; -} - -static inline void *alloc_cache_align(size_t n) -{ - void *res = 0; - if ((MEMALIGN(&res, L_CACHE_LINE_SIZE, cache_align(n)) < 0) || !res) { - fprintf(stderr, "MEMALIGN(%llu, %llu)", (unsigned long long)n, - (unsigned long long)cache_align(n)); - exit(-1); - } - return res; -} - -static inline void waiting_policy_sleep(volatile int *var) -{ - while (!(*var)) { - CPU_PAUSE(); - } -} - -static inline void waiting_policy_wake(volatile int *var) -{ - *var = UNLOCKED; - //assert(old == 0); -} - -mcs_mutex_t *mcs_mutex_create() -{ - mcs_mutex_t *impl = - (mcs_mutex_t *)alloc_cache_align(sizeof(mcs_mutex_t)); - impl->tail = 0; - return impl; -} - -static int __mcs_mutex_lock(mcs_mutex_t *impl, mcs_node_t *me) -{ - mcs_node_t *tail; - - //assert(me != NULL); - - me->next = LOCKED; - me->spin = 0; - - // The atomic instruction is needed when two threads try to put themselves - // at the tail of the list at the same time - tail = xchg_64((void *)&impl->tail, (void *)me); - - /* No one there? */ - if (!tail) { - return 0; - } - - /* Someone there, need to link in */ - tail->next = me; - COMPILER_BARRIER(); - - //waiting_policy_sleep(&me->spin); - while (!me->spin) { - CPU_PAUSE(); - } - - return 0; -} - -int mcs_mutex_lock(mcs_mutex_t *impl, mcs_node_t *me) -{ - int ret = __mcs_mutex_lock(impl, me); - //assert(ret == 0); - //DEBUG("[%d] Lock acquired posix=%p\n", cur_thread_id, &impl->posix_lock); - return ret; -} - -static void __mcs_mutex_unlock(mcs_mutex_t *impl, mcs_node_t *me) -{ - /* No successor yet? */ - if (!me->next) { - // The atomic instruction is needed if a thread between the previous if - // and now has enqueued itself at the tail - if (__sync_val_compare_and_swap(&impl->tail, me, 0) == me) - return; - - /* Wait for successor to appear */ - while (!me->next) { - CPU_PAUSE(); - } - } - - /* Unlock next one */ - //waiting_policy_wake(&me->next->spin); - me->next->spin = UNLOCKED; -} - -void mcs_mutex_unlock(mcs_mutex_t *impl, mcs_node_t *me) -{ - __mcs_mutex_unlock(impl, me); -} - -int mcs_mutex_destroy(mcs_mutex_t *lock) -{ - free(lock); - lock = NULL; - - return 0; -} diff --git a/benchmarks/specfs_bench/data/code/mcs.h b/benchmarks/specfs_bench/data/code/mcs.h deleted file mode 100644 index 38adc724..00000000 --- a/benchmarks/specfs_bench/data/code/mcs.h +++ /dev/null @@ -1,61 +0,0 @@ -/* - * The MIT License (MIT) - * - * Copyright (c) 2016 Hugo Guiroux - * - * Permission is hereby granted, free of charge, to any person obtaining a copy - * of his software and associated documentation files (the "Software"), to deal - * in the Software without restriction, including without limitation the rights - * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell - * copies of the Software, and to permit persons to whom the Software is - * furnished to do so, subject to the following conditions: - * - * The above copyright notice and this permission notice shall be included in - * all copies or substantial portions of the Software. - * - * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR - * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, - * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE - * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER - * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, - * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE - * SOFTWARE. - */ -#ifndef __MCS_H__ -#define __MCS_H__ - -#define _GNU_SOURCE - -#define NUMA_NODES 2 -#define CPU_NUMBER 32 -#define L_CACHE_LINE_SIZE 128 -#define LOCKED 0 -#define UNLOCKED 1 -#define SPINNING_THRESHOLD 2700LL - -#define r_align(n, r) (((n) + (r) - 1) & -(r)) -#define cache_align(n) r_align(n, L_CACHE_LINE_SIZE) -#define pad_to_cache_line(n) (cache_align(n) - (n)) -#define MEMALIGN(ptr, alignment, size) \ - posix_memalign((void **)(ptr), (alignment), (size)) - -typedef struct mcs_node { - struct mcs_node *volatile next; - char __pad[pad_to_cache_line(sizeof(struct mcs_node *))]; - volatile int spin __attribute__((aligned(L_CACHE_LINE_SIZE))); -} mcs_node_t __attribute__((aligned(L_CACHE_LINE_SIZE))); - -typedef struct mcs_mutex { - struct mcs_node *volatile tail - __attribute__((aligned(L_CACHE_LINE_SIZE))); -} mcs_mutex_t __attribute__((aligned(L_CACHE_LINE_SIZE))); - -mcs_mutex_t *mcs_mutex_create(); -int mcs_mutex_lock(mcs_mutex_t *impl, mcs_node_t *me); -void mcs_mutex_unlock(mcs_mutex_t *impl, mcs_node_t *me); -int mcs_mutex_destroy(mcs_mutex_t *lock); - -typedef mcs_mutex_t lock_mutex_t; -typedef mcs_node_t lock_context_t; - -#endif // __MCS_H__ diff --git a/benchmarks/specfs_bench/data/code/path/path.h b/benchmarks/specfs_bench/data/code/path/path.h deleted file mode 100644 index cf232207..00000000 --- a/benchmarks/specfs_bench/data/code/path/path.h +++ /dev/null @@ -1,10 +0,0 @@ -#ifndef _PATH_H -#define _PATH_H - -#include "inode.h" -#include "common.h" -#include "util.h" - -struct inode* locate(struct inode* cur, char* path[]); -struct inode* locate_hold(struct inode *cur, char *path[]); -#endif // _PATH_H \ No newline at end of file diff --git a/benchmarks/specfs_bench/data/code/util/util.h b/benchmarks/specfs_bench/data/code/util/util.h deleted file mode 100644 index 00d505b7..00000000 --- a/benchmarks/specfs_bench/data/code/util/util.h +++ /dev/null @@ -1,31 +0,0 @@ -#ifndef _UTIL_H -#define _UTIL_H - -#include -#include "common.h" -#include "mcs.h" - -unsigned char* malloc_page(); -char** malloc_dir_content(unsigned size); -char* malloc_buffer(unsigned len); -struct read_ret* malloc_readret(); -void fill_dir(struct inode* inum, char** dircontent); -void free_dirs(char *dirname[]); -struct inode* malloc_inode(int mode, unsigned maj, unsigned min); -char** calculate(char* srcpath[], char* dstpath[]); -void free_path(char** path); -int getlen(char* path[]); -void lock(struct inode* inum); -void unlock2dir (struct inode* srcdir, struct inode* dstdir); -void unlock(struct inode* inum); -void dispose_inode(struct inode* inum); -char** malloc_path(unsigned len); -void free_readret(struct read_ret *p); -struct entry *malloc_entry(); -void split_dirs_file(const char *path, char *dirname[], char *filename); -void split_dirs(const char *path, char *dirname[]); -unsigned int hash_name(char* name); -char* malloc_string(const char* name); -void free_entry(struct entry* en); -struct getattr_ret* malloc_getattr_ret(struct inode* inum, unsigned mode, unsigned size, unsigned maj, unsigned min); -#endif // _UTIL_H \ No newline at end of file diff --git a/benchmarks/specfs_bench/data/spec/common.header b/benchmarks/specfs_bench/data/spec/common.header deleted file mode 100644 index d15d05b4..00000000 --- a/benchmarks/specfs_bench/data/spec/common.header +++ /dev/null @@ -1,67 +0,0 @@ -string, stdio, stdlib, unistd, sys/syscall, assert - -#define FUSE_USE_VERSION 26 -#define FS_DATA ((struct fs_state *)fuse_get_context()->private_data) -#define LOCK_COUPLING - -#define FILE_MODE 1 -#define DIR_MODE 2 -#define CHR_MODE 3 -#define BLK_MODE 4 -#define SOCK_MODE 5 -#define FIFO_MODE 6 - -#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) - -typedef unsigned long long u64; -typedef struct entry { - char *name; - void *inum; - struct entry *next; -} entry; - -typedef struct indextb { - unsigned char *index[INDEXTB_NUM]; -} indextb; - -typedef struct dirtb { - struct entry *tb[DIRTB_NUM]; -} dirtb; - -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; - -typedef struct getattr_ret { - struct inode *inum; - unsigned mode; - unsigned size; - unsigned maj; - unsigned min; -} getattr_ret; - -typedef struct read_ret { - char *buf; - unsigned num; -} read_ret; - -extern struct inode *root_inum; - -struct fs_state { - FILE *logfile; -}; \ No newline at end of file diff --git a/benchmarks/specfs_bench/data/spec/file/file.header b/benchmarks/specfs_bench/data/spec/file/file.header deleted file mode 100644 index 74506099..00000000 --- a/benchmarks/specfs_bench/data/spec/file/file.header +++ /dev/null @@ -1,5 +0,0 @@ -common, util -void file_clear(struct inode *node, unsigned start, unsigned len); -void file_allocate(struct inode *node, unsigned offset, unsigned len); -void file_read(struct inode *node, unsigned offset, unsigned len, char *data); -void file_write(struct inode *node, unsigned offset, unsigned len, const char *data); diff --git a/benchmarks/specfs_bench/data/spec/inode/inode.header b/benchmarks/specfs_bench/data/spec/inode/inode.header deleted file mode 100644 index 79bce7e7..00000000 --- a/benchmarks/specfs_bench/data/spec/inode/inode.header +++ /dev/null @@ -1,7 +0,0 @@ -common, util, file -int inode_insert(struct inode* cur, struct inode* inum, char* name); -struct inode* inode_delete(struct inode* inum, char* name); -unsigned inode_write(struct inode* node, const char* buffer, unsigned len, unsigned offset); -void inode_truncate(struct inode* node, unsigned size); -struct read_ret* inode_read(struct inode* node, unsigned len, unsigned offset); -struct inode *inode_find(struct inode *node, char *name); diff --git a/benchmarks/specfs_bench/data/spec/interface-util/interface-util.header b/benchmarks/specfs_bench/data/spec/interface-util/interface-util.header deleted file mode 100644 index 5580a3f2..00000000 --- a/benchmarks/specfs_bench/data/spec/interface-util/interface-util.header +++ /dev/null @@ -1,8 +0,0 @@ -inode, common, util -int check_file(struct inode *inum); -void check_unlock (struct inode* parent, struct inode* src, struct inode* dst); -int check_ins(struct inode *cur, char *name); -int check_dir(struct inode *inum); -int check_src_exist_dst_delete(struct inode *srcdir, struct inode *dstdir, char *srcname, char *dstname); -int check_del(struct inode *cur, char *name); -int check_open(struct inode *inum, unsigned mode); diff --git a/benchmarks/specfs_bench/data/spec/interface/interface.header b/benchmarks/specfs_bench/data/spec/interface/interface.header deleted file mode 100644 index bf95c577..00000000 --- a/benchmarks/specfs_bench/data/spec/interface/interface.header +++ /dev/null @@ -1,10 +0,0 @@ -common, util, inode, interface-util, path -struct inode *atomfs_open(char *path[], unsigned mode); -int atomfs_truncate(char* path[], unsigned offset); -int atomfs_rename(char* srcpath[], char* dstpath[], char* srcname, char* dstname); -char **atomfs_readdir(char *path[]); -struct read_ret* atomfs_read(char* path[], unsigned size, unsigned offset); -int atomfs_ins(char* path[], char* name, int mode, unsigned maj, unsigned min); -int atomfs_del(char* path[], char* name); -struct getattr_ret* atomfs_getattr(char* path[]); -int atomfs_write(char* path[], const char* buf, unsigned size, unsigned offset); diff --git a/benchmarks/specfs_bench/data/spec/path/path.header b/benchmarks/specfs_bench/data/spec/path/path.header deleted file mode 100644 index e3e228ed..00000000 --- a/benchmarks/specfs_bench/data/spec/path/path.header +++ /dev/null @@ -1,3 +0,0 @@ -inode, common, util -struct inode* locate(struct inode* cur, char* path[]); -struct inode* locate_hold(struct inode *cur, char *path[]); diff --git a/benchmarks/specfs_bench/data/spec/util/util.header b/benchmarks/specfs_bench/data/spec/util/util.header deleted file mode 100644 index a10d7ca9..00000000 --- a/benchmarks/specfs_bench/data/spec/util/util.header +++ /dev/null @@ -1,24 +0,0 @@ -stdlib, common, mcs -unsigned char* malloc_page(); -char** malloc_dir_content(unsigned size); -char* malloc_buffer(unsigned len); -struct read_ret* malloc_readret(); -void fill_dir(struct inode* inum, char** dircontent); -void free_dirs(char *dirname[]); -struct inode* malloc_inode(int mode, unsigned maj, unsigned min); -char** calculate(char* srcpath[], char* dstpath[]); -void free_path(char** path); -int getlen(char* path[]); -void lock(struct inode* inum); -void unlock2dir (struct inode* srcdir, struct inode* dstdir); -void unlock(struct inode* inum); -void dispose_inode(struct inode* inum); -char** malloc_path(unsigned len); -void free_readret(struct read_ret *p); -struct entry *malloc_entry(); -void split_dirs_file(const char *path, char *dirname[], char *filename); -void split_dirs(const char *path, char *dirname[]); -unsigned int hash_name(char* name); -char* malloc_string(const char* name); -void free_entry(struct entry* en); -struct getattr_ret* malloc_getattr_ret(struct inode* inum, unsigned mode, unsigned size, unsigned maj, unsigned min); From b225324696b9818e13623019441f602ee95787f7 Mon Sep 17 00:00:00 2001 From: HarryZ Date: Mon, 20 Apr 2026 18:46:35 +0800 Subject: [PATCH 5/5] feat: refine readme file --- benchmarks/specfs_bench/README.md | 127 +++++++++++++++++++++++------- 1 file changed, 99 insertions(+), 28 deletions(-) diff --git a/benchmarks/specfs_bench/README.md b/benchmarks/specfs_bench/README.md index f7efe61a..fe44a4e8 100644 --- a/benchmarks/specfs_bench/README.md +++ b/benchmarks/specfs_bench/README.md @@ -1,50 +1,121 @@ -# SpecFS-Bench +# SpecFS Benchmark -SpecFS-Bench evaluates LLM capability on **spec-to-code generation** for filesystem C functions. +## Scenario Description -The pipeline contains two stages: +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. -1. **Generation**: For every `.spec` file under `data/spec`, ask the model to generate one corresponding C source file. -2. **Verification (LLM as Judge)**: Compare generated code against ground truth under `data/code` and output a simple score and diff summary. +### Task Details -## Data Layout +- **Input** + - Specification files (`.spec`) from `data/spec/` + - Generation / Judge prompt template + - Generation / Judge Model +- **Output** + - Generated C source file per spec under `outputs//generated/.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. -- `data/spec/**.spec`: formal function specifications and prompts. -- `data/code/**.c`: ground-truth implementation files (same relative path as spec, suffix changed to `.c`). +### Key Features -Example mapping: +- 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 -- `data/spec/file/file_read.spec` -- `data/code/file/file_read.c` +## Benchmark Setup -## Installation +### Prerequisites + +- Python 3.9+ +- LLM endpoint configured in `env.toml` + +### Configuration + +Copy the example config and fill in credentials: ```bash -cd benchmarks/specfs_bench -./install.sh +cp env.toml.example env.toml ``` -## Configuration +Edit `benchmarks/specfs/env.toml`: -Create `env.toml` in this benchmark directory (or use workspace-level `benchmarks/env.toml`). +```toml +[llm] +OPENAI_API_KEY = "your_key_here" +OPENAI_API_BASE = "your_url_here" +``` -You can copy from `env.toml.example` and fill your API credentials. +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. -## Run +### Install Dependencies ```bash -cd benchmarks/specfs_bench -./run.sh "gpt-4o" -# or use a separate judge model -./run.sh "openai/deepseek-chat" "gpt-4o" +cd benchmarks/specfs +./install.sh ``` -## Outputs +This script creates `.venv/` and installs `benchmarks/specfs/requirements.txt`. -Each run writes into `outputs/specfsbench____judge___/`: +### Run the Benchmark -- `generated/`: generated `.c` files preserving spec relative path. -- `generation_results.jsonl`: per-spec generation status. -- `judge_results.jsonl`: per-file judge results (score, verdict, differences). -- `summary.json`: aggregate metrics. +```bash +./run.sh +``` + +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____judge___/ +├── 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 +```