Skip to content

kwarg to @guppy for ordering requirements #1745

Description

@acl-cqc

e.g. max_effects=[...] or max_resources=[...]: a list being a subset of the available "tokens": initially, this could be the empty set, i.e. the only possible annotation would be max_effects=[]

  • Identify correct name for annotation (and the things in the list) - are they effects, resources, tokens, state, globals, etc.; is the annotation only_, max_, or just effects, or something like uses or affects, etc. (If you include something in max_effects but then don't use it, for linking purposes the function still has to take the token, so it's only a "max" for what happens inside it)
  • Semantics: such a function may call only functions that are also annotated with the same / a subset of effects/resources. Check in guppy compiler and raise error if not.
  • All side-effecting functions - qalloc/qfree/result/panic/etc. - are unannotated, i.e. max_effects=[] functions cannot call them.

Metadata

Metadata

Assignees

Labels

No labels
No labels

Type

No type
No fields configured for issues without a type.

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions