An asynchronous function can release every resource before it finishes and still hold one at the wrong time. Borrow a connection from a small pool, then wait for an unrelated network request, and that connection remains occupied while the function is d. A release call later in the function does little for the other callers waiting now.
Whether that is a problem depends on the resource. Plenty of APIs are designed to stay open across asynchronous work. For this example, we will require resources acquired through our API to be released before the acquiring function suspends.
In Following untrusted data through a database, the policy followed a value from a write to a later read. Here we need to follow an object's state: has this particular resource been released at this particular point?
Here is the problem:
import { acquireResource, releaseResource } from "./resource";
export async function refresh() {
const resource = acquireResource();
await rebuildIndex();
releaseResource(resource);
}
At the await, resource is still held. The awaited expression need not use it. JavaScript s the surrounding async function, leaving the resource's lifecycle unfinished while execution is suspended.
Describe the resource #
Bifrost's RQL policy language lets us describe this API's resource lifecycle. Our policy treats the object returned by acquireResource() as acquired, and the first argument to releaseResource() as released. We supply those meanings when we define the policy's endpoints. A function called releaseResource does not acquire special powers by having a reassuring name.
The demo keeps the API declarations in src/resource.ts. Its acquisition selector is:
:selector (rql :schema-version 1
(language typescript
(call-sites-to :proof proven
(enclosing-decl
(where "src/resource.ts"
(function :name "acquireResource"))))))
:binding return-value
The file and function select a declaration. call-sites-to :proof proven then selects calls that the resolver binds to that declaration, including through the import. Release uses the same structure for releaseResource, with :binding (argument :index 0).
Another API can use the same names. The reproduction includes an unrelated acquireResource and releaseResource; those calls do not become resource events for this policy.
The helpers give us concrete declarations and returned objects for the example. The policy defines the protocol we want to check. A production resource pool would need to implement the actual acquisition and release.
Observe the state at suspension #
The resource starts in held. A successful release moves it to released. Bifrost can observe async suspension as a protocol event:
(event :id suspend
:on (suspension-boundary :scope analysis-root)
:supersedes [])
The relevant transitions are:
(transition :from held :on release :to released)
(transition :from held :on suspend :to violated)
(transition :from released :on suspend :to released)
Release is observed after the call returns normally. At suspension, the policy checks the current state of the tracked object. In the first example, that state is still held, so the transition produces a finding at the await.
The release later in the function does not erase that finding. A separate check adds a second await after release: the first suspension remains the violation, while the second sees the released state.
The recordings show the actual released CLI running against each example. The first catches the resource held at suspension. Playback timing is adjusted for readability.
The first run completes with one finding at src/held.ts:6. It reports certainty: possible, proof: proven, and completeness: complete. The proof is a typestate witness under our declared protocol; the result does not predict a deadlock or how long the scheduler will leave the function d.
Release the same object #
Moving a release above the await only helps if it releases the resource being tracked:
export async function refresh() {
const resource = acquireResource();
const alias = resource;
releaseResource(alias);
await rebuildIndex();
}
This run completes with zero findings. Bifrost proves that alias refers to the acquired object, so release changes that object's protocol state. The variable name can change without losing the connection.
Releasing a different resource is another matter. In a two-resource check, releasing second before suspension leaves first held, and the policy reports one finding. Counting release calls, or checking that one appears before the await, would miss the distinction.
A conditional alias also needs care:
const chosen = flag ? first : second;
releaseResource(chosen);
await rebuildIndex();
On v0.12.0, this check returns two possible findings and an inconclusive run with partial_discovery. The release cannot certify both objects as released. The uncertainty remains visible rather than becoming a clean result.
Check the resource at the #
This policy observes suspension within the analysis root. It makes no eventual-release obligation, and the demonstrated scope does not cover cancellation cleanup, deferred callback effects, or resource ownership transported between procedures. Adapting it to a library requires selecting the actual API and checking that its resource semantics fit the model.
Checking that a function eventually calls releaseResource would miss the problem. We need to know whether the same object is still held when the function s. Tracking the object's state catches the first case, accepts release through an exact alias, and leaves the conditional alias inconclusive.
Appendix: reproduce the examples #
The examples and both recordings were run with the public Bifrost v0.12.0 release, after verifying its download checksum.
The full reproduction includes the source, policy, validation script, and JSON reports. Seven checks cover the violation, exact alias, wrong-object release, unrelated API, second suspension, conditional alias, and unsupported async iteration.
The for await control returns zero findings with capability_incomplete: that suspension shape is not lowered in this release. Those zero findings establish nothing about safety.