Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
12 changes: 12 additions & 0 deletions CHANGELOG.md
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,18 @@ All notable changes to EigenScript are documented here.
## [Unreleased]

### Added
- **Cooperative task seeded scheduling — increment 4 (#408).**
`task_sched_seed of n` switches the scheduler from FIFO round-robin to
picking the next ready task from a seeded, platform-independent PRNG
(splitmix64). The schedule stays **fully deterministic** — the same seed
produces the same interleaving on every run and replays byte-identically
with **zero tape `N` records** — but a *different* seed explores a
*different* ordering. This is the pluggable strategy hook a deterministic
simulation tester (liferaft) uses to search the interleaving space while
keeping every run reproducible. Without a seed the scheduler is
unchanged (the FIFO fast path is untouched), so existing programs behave
exactly as before. Completes the #408 primitives; next is the liferaft
differential-proof migration.
- **Cooperative task virtual time — increment 3 (#408).** `task_sleep of
ticks` suspends a task on a **logical clock**; `task_now of null` reads
it. The clock starts at 0 and only jumps *forward to the earliest
Expand Down
1 change: 1 addition & 0 deletions docs/BUILTINS.md
Original file line number Diff line number Diff line change
Expand Up @@ -578,6 +578,7 @@ Requires full build. Transformer model inference and training.
| `task_kill` | `task_kill of id` | Tear down task `id`: drop its mailbox, mark it dead, wake any joiner with an `interrupt` error. Returns 1 if killed, 0 for a finished/unknown/self target. |
| `task_sleep` | `task_sleep of ticks` | Suspend this task until the **virtual clock** advances by `ticks`. The clock is logical (discrete-event): it only jumps forward — to the earliest sleeper — when nothing else is runnable, so sleeping stays deterministic, not wall-clock. A negative sleep is treated as 0. A no-op when no task has been spawned. Forbidden inside an `arena_mark`…`arena_reset` scope. |
| `task_now` | `task_now of null` | The current virtual-clock value (a number; 0 before any `task_sleep`). Deterministic — reads a logical counter, records no nondeterminism. |
| `task_sched_seed` | `task_sched_seed of n` | Install a scheduling **seed**: the scheduler switches from FIFO round-robin to picking the next ready task from a seeded, platform-independent PRNG. Same seed ⇒ same interleaving (byte-identical run + replay, zero tape nondeterminism); a different seed explores a different ordering — the lever a deterministic simulation tester uses to search interleavings. No seed ⇒ unchanged FIFO. Typically called once at program start. Returns null. |

**Thread safety:** Values sent through a channel (or returned through
`thread_join`) are deep-COPIED via `val_clone_for_send` — messages are
Expand Down
37 changes: 37 additions & 0 deletions docs/SPEC.md
Original file line number Diff line number Diff line change
Expand Up @@ -1222,6 +1222,43 @@ print of (task_now of null)
30
```

### Seeded scheduling

By default the ready tasks run round-robin (FIFO). `task_sched_seed of n`
switches the scheduler to pick the next ready task from a seeded,
platform-independent PRNG. The schedule stays **fully deterministic** — the
same seed produces the same interleaving on every run and replays
byte-identically, recording no tape nondeterminism — but a *different* seed
explores a *different* ordering. This is the lever a deterministic simulation
tester uses to search the space of interleavings while keeping every run
reproducible. Without a seed the scheduler is unchanged, so existing programs
behave exactly as before.

```eigenscript
task_sched_seed of 42
order is []
define step(tag) as:
order is append of [order, tag]
task_yield of null
order is append of [order, tag]
return tag

a is task_spawn of [step, "a"]
b is task_spawn of [step, "b"]
c is task_spawn of [step, "c"]
task_join of a
task_join of b
task_join of c
print of order
```
```output
["b", "c", "a", "b", "c", "a"]
```

The same program with no seed prints the round-robin order
`["a", "b", "c", "a", "b", "c"]`; a different seed prints a different — but
equally reproducible — permutation.

## Buffers

`buffer of count` allocates a flat array of `count` nums (all 0).
Expand Down
35 changes: 35 additions & 0 deletions examples/task_seeded_schedule.eigs
Original file line number Diff line number Diff line change
@@ -0,0 +1,35 @@
# Seeded scheduling (#408). By default cooperative tasks run round-robin
# (FIFO): the next ready task is always the one that has waited longest. A
# deterministic simulation tester (DST) instead wants to EXPLORE many
# interleavings of the same concurrent program, each one perfectly
# reproducible. `task_sched_seed of n` switches the scheduler to pick the next
# ready task from a seeded, platform-independent PRNG:
#
# * same seed => the SAME interleaving on every run and under EIGS_REPLAY
# (still zero tape nondeterminism — the pick is a pure
# function of the seed and program order);
# * a different seed => a different ordering to test.
#
# So a DST can sweep seeds 0, 1, 2, ... to search the interleaving space while
# every failure it finds replays byte-for-byte. Without a seed the scheduler is
# unchanged (FIFO), so existing programs behave exactly as before.

task_sched_seed of 42

order is []
define step(tag) as:
order is append of [order, tag] # runs, records, then hands off
task_yield of null
order is append of [order, tag] # resumes after the others
return tag

a is task_spawn of [step, "a"]
b is task_spawn of [step, "b"]
c is task_spawn of [step, "c"]
task_join of a
task_join of b
task_join of c

# Under seed 42 the ready task chosen at each hand-off is not the FIFO one, so
# the recorded order is a deterministic permutation — the same on every run.
print of order
17 changes: 17 additions & 0 deletions src/builtins.c
Original file line number Diff line number Diff line change
Expand Up @@ -4663,6 +4663,22 @@ Value* builtin_task_now(Value *arg) {
return make_num(task_virtual_now());
}

/* task_sched_seed of n — install a scheduling seed. By default tasks run FIFO
* round-robin; with a seed the scheduler picks the next ready task
* pseudo-randomly from a deterministic PRNG. The interleaving stays
* reproducible (same seed → byte-identical run + replay, zero tape nondet); a
* DIFFERENT seed explores a different ordering — the lever a deterministic
* simulation tester uses to search interleavings. Typically called once at
* program start. Returns null. */
Value* builtin_task_sched_seed(Value *arg) {
if (!arg || arg->type != VAL_NUM) {
rt_error(EK_TYPE, 0, "task_sched_seed requires a number (the seed)");
return make_null();
}
task_sched_set_seed(arg->data.num);
return make_null();
}

/* Deterministic teardown of OS-resource handles, run once the program has
* finished executing (the full value world is still alive, so buffered-message
* decrefs are safe). Channels and thread handles live in the process handle
Expand Down Expand Up @@ -5672,6 +5688,7 @@ void register_builtins(Env *env) {
env_set_local_owned(env, "task_kill", make_builtin(builtin_task_kill));
env_set_local_owned(env, "task_sleep", make_builtin(builtin_task_sleep));
env_set_local_owned(env, "task_now", make_builtin(builtin_task_now));
env_set_local_owned(env, "task_sched_seed", make_builtin(builtin_task_sched_seed));
env_set_local_owned(env, "thread_join", make_builtin(builtin_thread_join));
env_set_local_owned(env, "channel", make_builtin(builtin_channel));
env_set_local_owned(env, "send", make_builtin(builtin_send));
Expand Down
43 changes: 41 additions & 2 deletions src/vm.c
Original file line number Diff line number Diff line change
Expand Up @@ -5129,6 +5129,8 @@ typedef struct {
int active; /* armed on first spawn */
int dead_letters; /* inc 2: sends to finished/unknown tasks */
double now; /* inc 3: virtual clock (logical, starts 0) */
int seeded; /* inc 4: 1 once task_sched_seed installs a seed */
uint64_t rng_state; /* inc 4: splitmix64 state for the seeded pick */
Task main_task; /* task 0 — save-buffer only, never "started" */
} TaskScheduler;

Expand Down Expand Up @@ -5182,10 +5184,47 @@ static void sched_ready_push(TaskScheduler *s, int id) {
s->rcount++;
}

/* Inc 4: splitmix64 — a deterministic, platform-independent integer PRNG for
* the seeded scheduling strategy. Pure integer arithmetic (no float, no OS
* entropy), so the pick sequence is a reproducible function of the installed
* seed + program order — the seeded schedule replays byte-identically and
* records no tape nondeterminism. */
static uint64_t sched_rng_next(TaskScheduler *s) {
uint64_t z = (s->rng_state += 0x9E3779B97F4A7C15ULL);
z = (z ^ (z >> 30)) * 0xBF58476D1CE4E5B9ULL;
z = (z ^ (z >> 27)) * 0x94D049BB133111EBULL;
return z ^ (z >> 31);
}

/* task_sched_seed: install a seed and switch the scheduler from FIFO
* round-robin to a seeded pseudo-random pick of the next ready task. Ensures
* the scheduler exists so the seed sticks even when set before the first
* task_spawn. The interleaving stays deterministic — a DST varies the seed to
* explore different interleavings, each fully reproducible. */
void task_sched_set_seed(double seed) {
TaskScheduler *s = sched_ensure();
s->rng_state = (uint64_t)(int64_t)seed; /* integer seeds; fractions truncate */
s->seeded = 1;
}

static int sched_ready_pop(TaskScheduler *s) {
if (s->rcount == 0) return -1;
int id = s->ready[s->rhead];
s->rhead = (s->rhead + 1) % TASK_READY_MAX;
if (!s->seeded || s->rcount == 1) {
/* Default FIFO: O(1) head pop — the fast path, unchanged. */
int id = s->ready[s->rhead];
s->rhead = (s->rhead + 1) % TASK_READY_MAX;
s->rcount--;
return id;
}
/* Seeded strategy: pick a pseudo-random ready task, then compact the hole
* by shifting the suffix down one (order-preserving among the rest). O(n)
* in the ready count, which is tiny and only paid in DST/seeded mode. */
int idx = (int)(sched_rng_next(s) % (uint64_t)s->rcount);
int id = s->ready[(s->rhead + idx) % TASK_READY_MAX];
for (int k = idx; k < s->rcount - 1; k++) {
s->ready[(s->rhead + k) % TASK_READY_MAX] =
s->ready[(s->rhead + k + 1) % TASK_READY_MAX];
}
s->rcount--;
return id;
}
Expand Down
2 changes: 2 additions & 0 deletions src/vm.h
Original file line number Diff line number Diff line change
Expand Up @@ -453,6 +453,8 @@ int task_do_kill(int tid); /* deterministic teardown of `tid`; 0 = bad
/* Inc 3 virtual time (builtins.c task_sleep/task_now). */
void task_request_sleep(double ticks); /* current task sleeps until virtual now + ticks */
double task_virtual_now(void); /* current virtual-clock value (0 with no scheduler) */
/* Inc 4 seeded scheduling strategy (builtins.c task_sched_seed). */
void task_sched_set_seed(double seed); /* install a seed → seeded pick; ensures the scheduler */

/* ---- Public API ---- */

Expand Down
22 changes: 22 additions & 0 deletions tests/run_all_tests.sh
Original file line number Diff line number Diff line change
Expand Up @@ -2179,6 +2179,28 @@ else
FAIL=$((FAIL + 1))
fi

# #408 increment 4 seeded scheduling: task_sched_seed makes the scheduler pick
# the next ready task from a seeded PRNG. The seeded schedule must be identical
# on two fresh processes, replay byte-identically, record ZERO tape 'N' records,
# and differ from the FIFO round-robin order (proving the seed actually reorders).
TOTAL=$((TOTAL + 1))
SS_EX=../examples/task_seeded_schedule.eigs
SS_TAPE=$(mktemp -t eigs_ss.XXXXXX)
SSA=$(./eigenscript "$SS_EX" </dev/null 2>&1)
SSB=$(./eigenscript "$SS_EX" </dev/null 2>&1)
EIGS_TRACE="$SS_TAPE" ./eigenscript "$SS_EX" </dev/null >/dev/null 2>&1
SSR=$(EIGS_REPLAY="$SS_TAPE" ./eigenscript "$SS_EX" </dev/null 2>&1)
SS_NREC=$(grep -c '^N ' "$SS_TAPE" 2>/dev/null)
rm -f "$SS_TAPE"
if [ "$SSA" = "$SSB" ] && [ "$SSA" = "$SSR" ] && [ "$SS_NREC" -eq 0 ] && \
[ "$SSA" = '["b", "c", "a", "b", "c", "a"]' ]; then
echo " PASS: seeded scheduling is deterministic, replays, reorders vs FIFO (#408 inc4)"
PASS=$((PASS + 1))
else
echo " FAIL: seeded scheduling diverged/replayed wrong/leaked nondet (rec=$SS_NREC, out=$SSA)"
FAIL=$((FAIL + 1))
fi

# [105] Builtin contract fixes (#312 negative indices, #316 predicate
# type-rejection, #317 min/max N-ary reduction) + #314: a directory as the
# script path must take the clean cannot-read-file exit, not xmalloc's
Expand Down
45 changes: 45 additions & 0 deletions tests/test_tasks.eigs
Original file line number Diff line number Diff line change
Expand Up @@ -284,4 +284,49 @@ define lone() as:
return 7
assert_eq of [task_join of (task_spawn of lone), 7, "a lone sleeper is woken by the clock, not a deadlock"]

# ============================================================================
# Increment 4: the seeded scheduling strategy (task_sched_seed).
# MUST be the last section: seeding is sticky (global, no off-switch), so it
# would change the FIFO tie-breaks the earlier sections rely on. With a seed
# the scheduler picks the next ready task from a deterministic PRNG — same seed
# => same interleaving, a different seed => a different ordering.
# ============================================================================
define step(tag) as:
sched_order is append of [sched_order, tag]
task_yield of null
sched_order is append of [sched_order, tag]
return tag

# --- seed 42 yields its specific deterministic permutation (pins the PRNG) ---
task_sched_seed of 42
sched_order is []
sa is task_spawn of [step, "a"]
sb is task_spawn of [step, "b"]
sc is task_spawn of [step, "c"]
task_join of sa
task_join of sb
task_join of sc
assert_eq of [sched_order, ["b", "c", "a", "b", "c", "a"], "seed 42 gives its deterministic permutation"]
assert_true of [not (sched_order == ["a", "b", "c", "a", "b", "c"]), "seeded order differs from FIFO round-robin"]

# --- re-seeding with a different seed gives a different (still deterministic) order ---
task_sched_seed of 7
sched_order is []
s2a is task_spawn of [step, "a"]
s2b is task_spawn of [step, "b"]
s2c is task_spawn of [step, "c"]
task_join of s2a
task_join of s2b
task_join of s2c
assert_eq of [sched_order, ["a", "b", "c", "a", "c", "b"], "seed 7 gives a different deterministic permutation"]

# --- task_sched_seed requires a number ---
seed_threw is 0
try:
task_sched_seed of "not a number"
catch e:
seed_threw is 1
assert_eq of [e.kind, "type_mismatch", "task_sched_seed rejects a non-number seed"]
assert_eq of [seed_threw, 1, "task_sched_seed of a non-number raises"]

test_summary of null
Loading