Early stage · under heavy development Serene is a general-purpose, pure functional language with dependent types and a lispy surface syntax — built on Quantitative Type Theory.
The fiber subsystem now has a mutex to synchronize access to share resources. Similar to a thread level mutex, but in the context of a fiber.
An unlucky fiber which loses the races to acquire the lock will be suspended until the lock is released. When it awakes, the lock will be given to it.
See the runtime API and the exmaple 14 for details.
I've just wrapped up a three-part series on my personal blog about how concurrency works inside Serene's runtime - from picking the core abstraction all the way to a working HTTP server built on it.
If you've ever wondered why Serene uses fibers, how they can suspend across JIT and foreign C frames without function colouring, or how the scheduler and IO reactor fit together, this is the deep dive:
Part 1 — Choosing the Building Blocks A tour of the popular concurrency building blocks — threads, callbacks, async/await — what each one costs, and why fibers won.
Part 2 — Fibers, the Scheduler and the Reactor Inside Serene's fibers: frozen call chains, guard pages, a scheduler that knows nothing, and the IO Reactor that feeds it.
Part 3 — A Tiny HTTP Server Putting the fibers and IO Reactor to work in a small HTTP server that spawns a fiber per connection.
Best read in order, but each part stands on its own. Feedback welcome!
Serene's runtime is now can be used as a generic, standalone library; and can be utilized in any program. It licensed under the GNU LGPL v3.
It also splits cleanly. Build it with -Dwith-serene=disabled and you get just the generic substrate that does not include any Serene specific APIs.
So the pieces that were always general-purpose are now usable on their own. Pull in libserene.runtime through pkg-config and you're all set.
For more info check the runtime guide out.
The runtime now has an M:N, work-stealing fiber scheduler: stackful, cooperative fibers multiplexed across OS-thread workers, each with its own local run queue and work stealing between them. See the runtime API and the language report for details.
lscz2's pipeline is now organised around a graph. Namespaces are the graph's nodes, terms are added to it as they are checked, and evaluated values are fed back into the graph as values.
This end-to-end loop — Syntax → Expr (Semantic) → core terms → values — replaces the old linear pass structure and better matches how a dependently typed program is actually elaborated.
The stage-0 compiler has been ported from Haskell (lscz) to Idris2 (lscz2). With a dependently typed host language we can express Serene's type theory directly rather than encoding it.
This phase brought an elaborator from the high-level surface language down to the corett core, a bidirectional type checker for Kernel.TT, and the Parser and compiler Pipeline ported over to Idris2. Serene is now being built on Quantitative Type Theory — see the language report.