microsoft / armada

Armada is a tool for writing, and proving correct, high-performance concurrent programs.

Overview

Safely writing high-performance concurrent programs is notoriously difficult. To aid developers, we introduce Armada, a language and tool designed to formally verify such programs with relatively little effort. Via a C-like language that compiles to the C subset ClightTSO and a small-step, state-machine-based semantics, Armada gives developers the flexibility to choose arbitrary memory layout and synchronization primitives so they are never constrained in their pursuit of performance. To reduce developer effort, Armada leverages SMT-powered automation and a library of powerful reasoning techniques, including rely-guarantee, TSO elimination, reduction, and alias analysis. All these techniques are proven sound, and Armada can be soundly extended with additional strategies over time. Using Armada, we verify four concurrent case studies and show that we can achieve performance equivalent to that of unverified code.

You can read more about Armada in our PLDI '20 paper, which ACM will publish on June 17, 2020:

Jacob R. Lorch, Yixuan Chen, Manos Kapritsos, Bryan Parno, Shaz Qadeer, Upamanyu Sharma, James R. Wilcox, and Xueyuan Zhao. 2020. Armada: Low-Effort Verification of High-Performance Concurrent Programs. In Proceedings of the 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI '20), June 15-20, 2020, London, UK. ACM, New York, NY, USA, 14 pages. https://doi.org/10.1145/3385412.3385971

Getting started

To build Armada, please follow the detailed instructions documented in BUILD.md.

To use Armada, you'll need the following tools:

• .NET 5.0 (runtime for both Armada and Dafny)
• pip (needed for installing scons)
• scons (installable by running pip install scons)
• Dafny v3.2.0 (available at https://github.com/dafny-lang/dafny)

Generating and testing proofs

To use the Armada tool to generate proofs for all the included test Armada files (Test/*/*.arm), run, from the Armada top-level directory, scons -j <n> -f SConstruct1 where <n> is the number of threads you want scons to use.

To verify all the generated proofs, run, from the same directory, scons -j <n> -f SConstruct2 --DAFNYPATH=<dafny-path> where <dafny-path> is the directory containing the Dafny.exe/Dafny.dll binary you installed.

If this second scons finishes without printing an error message, this means that everything worked. If it reports an error, this is likely due to running on a machine without enough memory, so try again with fewer threads.

Compilation, performance evaluation, and graph generation

To build the queue benchmarks, run them, and generate the performance graphs, run python3 run_benchmarks.py in the Test/qbss_benchmark/ directory. This will produce a file qbss_performance_graph.pdf with the performance graph.

Contributing

This project welcomes contributions and suggestions. Most contributions require you to agree to a Contributor License Agreement (CLA) declaring that you have the right to, and actually do, grant us the rights to use your contribution. For details, visit https://cla.opensource.microsoft.com.

When you submit a pull request, a CLA bot will automatically determine whether you need to provide a CLA and decorate the PR appropriately (e.g., status check, comment). Simply follow the instructions provided by the bot. You will only need to do this once across all repos using our CLA.

This project has adopted the Microsoft Open Source Code of Conduct. For more information see the Code of Conduct FAQ or contact [email protected] with any additional questions or comments.

armada's Issues

Can't subtract integer from pointer into array

Currently, you can add an integer to a pointer into an array but you can't subtract one. So instead of, say, p - 1, you have to use the somewhat awkward expression p + (-1).

Set up CI

Set up continuous integration (e.g. Github Actions) that builds Armada files and verifies the generated and included Dafny files. It would be nice to always know if anything on the main branch is broken and to have CI for vetting proposed changes.

Can't subtract pointers into same array

Currently, it's not supported to subtract two pointers, even if it's well-defined because those pointers point into the same array. For instance, you can't do:

  var a: uint32[10];
  ghost var i: int;
  i := &a[5] - &a[3]; // Should give 2

Overview should mention that the target is standard C (ClightTSO)

I suggest that the Overview section of the README.md should mention that Armada targets standard C (specifically the ClightTSO subset). At first I got the impression Armada was less ambitious than it really is.

(I heard of Armada through this HackerNews thread.)

Concrete levels can atomically return multiple shared locations

Armada's concrete-level checker doesn't prevent return statements that access multiple shared locations, such as return s where s is an addressable struct.

The proper fix is probably to just disallow arguments in return statements. One should return values by assigning them to output parameters, then using a bare return statement.

Can't subtract pointers into the same array

In C, one can subtract pointers from each other. We don't want to allow this for arbitrary pointers in Armada, but it makes sense to allow it for pointers into the same array. After all, we already allow adding an integer to a pointer to an array element.

It would be useful to support subtracting pointers, with undefined-behavior semantics if they don't point into the same array.

Shared-memory access counting too conservative

Armada makes sure that concrete levels are compilable. One of the ways it does this is by ensuring that each instruction accesses no more than one shared-memory location. However, the code to do this is too conservative, sometimes considering an instruction to access multiple shared-memory locations when it actually doesn't.

For instance, if m and n are shared-memory locations, then it's not appropriate to read both m and n in the same instruction. But it should be legal to read their addresses in the same instruction, like MethodCall(&m, &n). Nevertheless, this is currently flagged as an illegal multiple shared-memory access. In other words, expressions like &m, &n, &arr[3], and &((*p).f) are counted as shared-memory accesses even when they don't involve accesses to shared memory.

Another instance of overcounting is when a method call accesses shared memory during both the call and the assignment of return variables. Currently, the instruction m := MethodCall(n) is flagged as an illegal multiple shared-memory access. But it would be fine to allow this, since the call step is modeled as a separate step from the assignment-of-return-variables step.

No support for thread-local storage

Armada doesn't support thread-local storage constructs. It would be useful to remedy this.

Taking address of array causes crash

The Armada program below crashes the state-machine translator while it's in HeadWithProxyArgs, since HeadWithProxyArgs doesn't support the sized-array case. Instead, Armada should report a bug due to the developer trying to take the address of an array (instead of an array element).

include "../../Armada/ArmadaCommonDefinitions.dfy"

structs SharedStructs {
  struct S {
    var x: uint32;
  }
}

level Test using SharedStructs {
  method main ()
  {
    var a: S[10];
    var p: ptr<S>;
    p := &a;
  }
}

Problem with C generation

I found problems with C++ generation in Armada.
First, Test/qbss_benchmark/queue.patch is out of date. // namespace _9_SharedStructs should be replaced with // namespace _12_SharedStructs.

Besides, I got queue.c:93:3: error: implicit declaration of function 'LFDS711_PAL_ASSERT' is invalid in C99 [-Werror,-Wimplicit-function-declaration]. Does it rely on the platform or the version of gcc?

Also, I found that there is a potential bug in Compiler.cs/CreateLvalue(Expression lhs, TargetWriter wr). With the following code:

*(errors_ptr + i) := 0;

CreateLvalue couldn't handle BinaryExpr(+), and got an exception.

dafny version

Hi,

Which version of dafny should be used for the current code?
I have downloaded dafny 2.3.0 and add the *.dll to VS2017.
I got errors below when building the code.

Severity Code Description Project File Line Suppression State
Error Application Configuration file "app.config" is invalid. Could not find file 'C:\Users\andyj\Armada-master\Source\ArmadaDriver\app.config'. Armada C:\Users\andyj\Armada-master\Source\ArmadaDriver\app.config
Error CS1503 Argument 2: cannot convert from 'string' to 'Microsoft.Boogie.Variable' ArmadaPipeline C:\Users\andyj\Armada-master\Source\Armada\Translator.cs 14327 Active
Error CS1503 Argument 2: cannot convert from 'string' to 'Microsoft.Boogie.Variable' ArmadaPipeline C:\Users\andyj\Armada-master\Source\Armada\Translator.cs 13491 Active
Error CS1503 Argument 2: cannot convert from 'string' to 'Microsoft.Boogie.Variable' ArmadaPipeline C:\Users\andyj\Armada-master\Source\Armada\Translator.cs 7274 Active
Error CS1503 Argument 2: cannot convert from 'string' to 'Microsoft.Boogie.Variable' ArmadaPipeline C:\Users\andyj\Armada-master\Source\Armada\Translator.cs 5791 Active

Assume at end of if clause attaches to subsequent statement

If an if statement has no else clause, and its then clause ends in an assume statement, then the enabling condition is attached to the first statement following the if. In other words, that if-following statement will block on the condition whether or not the then branch was taken. This is non-intuitive and thus likely to be surprising and unexpected to developers.

Similarly, if an if statement has an else clause, and that else clause ends in an assume statement, the enabling condition is attached to the first statement following the if. This is also non-intuitive.

For these reasons, it seems useful to ensure that there's always a PC at the end of each then and else clause that's distinct from the PC of the subsequent instruction. That will require adding some extra steps that do nothing other than advance the PC from the clause-ending PC to the subsequent one.

Can't specify inductive invariant sets

Our automatic proof generator can't tell which invariants' proofs are dependent on which other invariants. So they always conservatively generate proofs that will work even if each invariant depends on each other one.

For instance, suppose we have to prove invariants I1, I2, and I3. It may be that I1 is inductive all by itself, but it could also be that it's not but I1 && I2 && I3 is inductive. We don't know which invariants together constitute an inductive invariant, so to prove that I1 is an invariant with an automatically-generated lemma, we have to emit one that proves I1 && I2 && I3 ==> I1'.

It would be useful to let the developer specify, in the recipe, that to prove a certain invariant you only need to use a certain specified set of other invariants. This would generate proofs that are faster to verify. Indeed, in some cases this feature may be necessary to prevent invariant proofs from timing out.

It might also be useful to specify that a certain invariant is not needed in any invariant proofs except its own and ones it's explicitly specified to be needed in. This way, if a certain invariant introduces too many facts (e.g., with a loosely-triggered quantifier), the developer can limit its use this way.

Generated files hard to distinguish from developer-written ones

Generated files, like regular Dafny files, end in .dfy. So it's hard to distinguish them from developer-written .dfy files like barrier/extra.dfy. As a result, sometimes developers forget to check in the .dfy files they've written.

It would be useful if generated Dafny files were named specially, e.g., if they all ended in .g.dfy. Then, it would be straightforward to have a .gitignore entry that covered those files but not developer-written ones.

Customizations are per-lemma, not per-instruction

Currently, a lemma customization is specific to a particular lemma. However, it would be useful to have a customization apply to all generated lemmas involving a certain instruction. For instance, if an instruction performs a certain piece of tricky modulo arithmetic, the developer may find it useful to request invocation of a certain lemma about modulo arithmetic in all lemmas involving that instruction.

Concrete levels can include non-external atomic methods

The concrete-level checker doesn't raise an error if the level contains an {:atomic} method that isn't {:extern}. But it should, since the compiler can't compile an {:atomic} method (at least, not so that its calls and returns are indeed nonyielding points).

Grammar railroad diagram

Looking for people using CocoR I found this project and I've done a experimental tool to convert CocoR grammars to a kind of EBNF understood by https://www.bottlecaps.de/rr/ui to generate railroad diagrams see bellow the converted and with some hand made changes of Armada.atg to allow view it at https://www.bottlecaps.de/rr/ui the order of the rules could be changed to a better view of the railroad diagrams. Copy and paste the EBNF bellow on https://www.bottlecaps.de/rr/ui tab Edit Grammar then switch to the tab View Diagram.

I implemented the generation of the Parser.ebnf on this fork of CocoR Csharp https://github.com/mingodad/CocoR-CSharp and you can download the railroad generator to generate offline using Java here https://www.bottlecaps.de/rr/download/rr-1.63-java8.zip (link from the https://www.bottlecaps.de/rr/ui on tab Welcome).

Coco.exe -genRREBNF Armada.atg
java -jar rr.war -out:Armada.atg.xhtml Parser.ebnf

Also any feedback on the CocoR extensions are welcome !

Cheers !

//
// EBNF generated by CocoR parser generator to be viewed with https://www.bottlecaps.de/rr/ui
//

//
// productions
//

Armada ::= ( "include" stringToken )* ( TopDecl )* EOF 
TopDecl ::= ( DeclModifier )* ( SubModuleDecl | ClassDecl | DatatypeDecl | NewtypeDecl | OtherTypeDecl | IteratorDecl | TraitDecl | ClassMemberDecl | RefinementConstraintDecl | ArmadaProofDecl ) 
DeclModifier ::= ( "abstract" | ghost | static | protected | "noaddr" ) 
SubModuleDecl ::= ( ( module | "layer" | "level" | "structs" | "proof" ) ( Attribute )* NoUSIdent ( dot NoUSIdent )* ( "using" NoUSIdent )? ( "refines" ModuleName )? lbrace ( TopDecl )* rbrace | import ( "opened" )? ModuleName ( ( QualifiedModuleExportSuffix )? | "=" QualifiedModuleExport | colon QualifiedModuleExport ) ( semi )? | export ( ExportIdent )? ( ( "provides" ( ModuleExportSignature ( comma ModuleExportSignature )* | star ) | "reveals" ( ModuleExportSignature ( comma ModuleExportSignature )* | star ) | "extends" ExportIdent ( comma ExportIdent )* ) )* ) 
ClassDecl ::= "struct" ( Attribute )* NoUSIdent ( GenericParameters )? ( "extends" Type ( comma Type )* )? lbrace ( ( DeclModifier )* ClassMemberDecl )* rbrace 
DatatypeDecl ::= ( datatype | codatatype ) ( Attribute )* NoUSIdent ( GenericParameters )? "=" ( verticalbar )? DatatypeMemberDecl ( verticalbar DatatypeMemberDecl )* ( TypeMembers )? 
NewtypeDecl ::= newtype ( Attribute )* NoUSIdent "=" ( NoUSIdent ( colon Type )? verticalbar Expression ( ( ghost )? witness Expression )? ( TypeMembers )? | Type ( TypeMembers )? ) 
OtherTypeDecl ::= type ( Attribute )* NoUSIdent ( TypeParameterCharacteristics )* ( GenericParameters )? ( "=" ( NoUSIdent ( colon Type )? verticalbar Expression ( ( ghost )? witness Expression )? | Type ) )? ( semi )? 
IteratorDecl ::= iterator ( Attribute )* NoUSIdent ( ( GenericParameters )? Formals ( ( "yields" | "returns" ) Formals )? | ellipsis ) ( IteratorSpec )* ( BlockStmt )? 
TraitDecl ::= trait ( Attribute )* NoUSIdent ( GenericParameters )? lbrace ( ( DeclModifier )* ClassMemberDecl )* rbrace 
ClassMemberDecl ::= ( FieldDecl | ConstantFieldDecl | FunctionDecl | MethodDecl | GlobalInvariantDecl | YieldPredicateDecl | UniversalStepConstraintDecl ) 
RefinementConstraintDecl ::= "refinement_constraint" stringToken 
ArmadaProofDecl ::= ( "refinement" NoUSIdent NoUSIdent | "include_file" stringToken ( "which_includes" stringToken ( comma stringToken )* )? | "import_module" NoUSIdent ( "which_imports" NoUSIdent ( comma NoUSIdent )* )? | "extra" NoUSIdent stringToken | "inductive_invariant" ( Attribute )* NoUSIdent ( stringToken )? ( "depends_on" NoUSIdent ( comma NoUSIdent )* )? | "use_regions" | "use_address_invariant" | "chl_invariant" ( Attribute )* NoUSIdent ( stringToken )? | "chl_local_invariant" ( Attribute )* NoUSIdent NoUSIdent ( stringToken )? | "chl_yield_pred" ( Attribute )* NoUSIdent ( stringToken )? | "chl_precondition" ( Attribute )* NoUSIdent NoUSIdent ( stringToken )? | "chl_postcondition" ( Attribute )* NoUSIdent NoUSIdent ( stringToken )? | "chl_loop_modifies" ( Attribute )* NoUSIdent NoUSIdent ( stringToken )? | "auxiliary" NoUSIdent stringToken stringToken stringToken stringToken | "weakening" ( LabelIdent ( comma LabelIdent )* )? | "starweakening" ( "statements" LabelIdent ( comma LabelIdent )* )? ( "variables" LabelIdent ( comma LabelIdent )* )? | "var_hiding" NoUSIdent ( comma NoUSIdent )* | "stack_var_hiding" NoUSIdent NoUSIdent ( comma NoUSIdent )* | "var_intro" NoUSIdent ( comma NoUSIdent )* | "stack_var_intro" NoUSIdent NoUSIdent ( stringToken )? | "reduction" ( "phase1" NoUSIdent ( "-" NoUSIdent )? ( comma NoUSIdent ( "-" NoUSIdent )? )* )? ( "phase2" NoUSIdent ( "-" NoUSIdent )? ( comma NoUSIdent ( "-" NoUSIdent )? )* )? | "combining" NoUSIdent NoUSIdent NoUSIdent | "field_hiding" NoUSIdent NoUSIdent | "field_intro" NoUSIdent NoUSIdent | "assume_intro" ( LabelIdent ( comma LabelIdent )* )? | "chl" | "critsec" NoUSIdent | "tso_elim" PeriodSeparatedIdentifierList stringToken ) 
Attribute ::= lbracecolon NoUSIdent ( Expressions )? rbrace 
NoUSIdent ::= ident 
ModuleName ::= Ident 
QualifiedModuleExportSuffix ::= ( dot ModuleName ( dot ModuleName )* | backtick ( ExportIdent | lbrace ExportIdent ( comma ExportIdent )* rbrace ) ) 
QualifiedModuleExport ::= ModuleName ( QualifiedModuleExportSuffix )? 
ExportIdent ::= FuMe_Ident 
ModuleExportSignature ::= TypeNameOrCtorSuffix ( dot TypeNameOrCtorSuffix )? 
TypeNameOrCtorSuffix ::= ( ident | digits ) 
Ident ::= ident 
GenericParameters ::= openAngleBracket ( Variance )? NoUSIdent ( TypeParameterCharacteristics )* ( comma ( Variance )? NoUSIdent ( TypeParameterCharacteristics )* )* closeAngleBracket 
Type ::= TypeAndToken 
GlobalInvariantDecl ::= invariant NoUSIdent FunctionBody 
FunctionBody ::= lbrace Expression rbrace 
YieldPredicateDecl ::= "yield_predicate" NoUSIdent FunctionBody 
UniversalStepConstraintDecl ::= "universal_step_constraint" NoUSIdent ( FunctionBody | stringToken ) 
LabelIdent ::= ( NoUSIdent | digits ) 
PeriodSeparatedIdentifierList ::= NoUSIdent ( dot NoUSIdent )* 
FieldDecl ::= var ( Attribute )* FIdentType ( gets Expression )? ( comma FIdentType ( gets Expression )? )* OldSemi 
ConstantFieldDecl ::= const ( Attribute )* CIdentType ( gets Expression )? OldSemi 
FunctionDecl ::= ( twostate )? ( function ( method )? ( Attribute )* FuMe_Ident ( ( GenericParameters )? Formals colon ( openparen GIdentType closeparen | Type ) | ellipsis ) | predicate ( method )? ( Attribute )* NoUSIdent ( ( GenericParameters )? ( Formals )? ( colon )? | ellipsis ) | inductive predicate ( Attribute )* FuMe_Ident ( ( GenericParameters )? ( KType )? Formals ( colon )? | ellipsis ) | copredicate ( Attribute )* NoUSIdent ( ( GenericParameters )? ( KType )? Formals ( colon )? | ellipsis ) ) ( FunctionSpec )* ( FunctionBody )? 
MethodDecl ::= ( method | lemma | colemma | "comethod" | inductive lemma | twostate lemma | constructor | "destructor" ) ( Attribute )* ( FuMe_Ident )? ( ( GenericParameters )? ( KType )? Formals ( "returns" Formals )? | ellipsis ) ( MethodSpec )* ( ( DividedBlockStmt | BlockStmt ) )? 
DatatypeMemberDecl ::= ( Attribute )* NoUSIdent ( FormalsOptionalIds )? 
TypeMembers ::= lbrace ( ( DeclModifier )* ClassMemberDecl )* rbrace 
FormalsOptionalIds ::= openparen ( TypeIdentOptional ( comma TypeIdentOptional )* )? closeparen 
FIdentType ::= ( WildIdent | digits ) colon Type 
Expression ::= EquivExpression ( semi Expression )? 
OldSemi ::= ( semi )? 
CIdentType ::= ( WildIdent | digits ) ( colon Type )? 
TypeParameterCharacteristics ::= openparen TPCharOption ( comma TPCharOption )* closeparen 
GIdentType ::= ( ( ghost | "new" ) )* IdentType 
IdentType ::= WildIdent colon Type 
WildIdent ::= ident 
LocalIdentTypeOptional ::= WildIdent ( colon Type )? 
IdentTypeOptional ::= WildIdent ( colon Type )? 
TypeIdentOptional ::= ( ghost )? ( TypeAndToken ( colon Type )? | digits colon Type ) 
TypeAndToken ::= ( bool | char | int | nat | real | ORDINAL | bvToken | set OptGenericInstantiation | iset OptGenericInstantiation | multiset OptGenericInstantiation | seq OptGenericInstantiation | "ptr" OptGenericInstantiation | string | object | object_q | map OptGenericInstantiation | imap OptGenericInstantiation | arrayToken OptGenericInstantiation | arrayToken_q OptGenericInstantiation | openparen ( Type ( comma Type )* )? closeparen | NameSegmentForTypeName ( dot TypeNameOrCtorSuffix OptGenericInstantiation )* ) ( lbracket Nat rbracket )? ( ( "~>" | "-->" | "->" ) Type )? 
Formals ::= openparen ( GIdentType ( comma GIdentType )* )? closeparen 
IteratorSpec ::= ( reads ( Attribute )* FrameExpression ( comma FrameExpression )* OldSemi | modifies ( Attribute )* FrameExpression ( comma FrameExpression )* OldSemi | ( "free" )? ( "yield" )? ( requires ( LabelIdent colon )? Expression OldSemi | ensures ( Attribute )* Expression OldSemi ) | decreases ( Attribute )* DecreasesList OldSemi ) 
BlockStmt ::= lbrace ( Stmt )* rbrace 
Variance ::= ( star | "+" | "!" | "-" ) 
TPCharOption ::= ( eq | digits | "!" "new" ) 
FuMe_Ident ::= ( NoUSIdent | digits ) 
KType ::= lbracket ( nat | ORDINAL ) rbracket 
MethodSpec ::= ( modifies ( Attribute )* FrameExpression ( comma FrameExpression )* OldSemi | ( "free" )? ( requires ( Attribute )* ( LabelIdent colon )? Expression OldSemi | ensures ( Attribute )* Expression OldSemi ) | decreases ( Attribute )* DecreasesList OldSemi | reads Expression ( comma Expression )* OldSemi | "awaits" Expression ( comma Expression )* OldSemi | "undefined_unless" Expression ( comma Expression )* OldSemi ) 
DividedBlockStmt ::= lbrace ( Stmt )* ( "new" semi ( Stmt )* )? rbrace 
FrameExpression ::= ( Expression ( backtick Ident )? | backtick Ident ) 
DecreasesList ::= PossiblyWildExpression ( comma PossiblyWildExpression )* 
OptGenericInstantiation ::= ( GenericInstantiation )? 
NameSegmentForTypeName ::= Ident OptGenericInstantiation 
Nat ::= ( digits | hexdigits ) 
GenericInstantiation ::= openAngleBracket Type ( comma Type )* closeAngleBracket 
FunctionSpec ::= ( requires ( Attribute )* Expression OldSemi | reads PossiblyWildFrameExpression ( comma PossiblyWildFrameExpression )* OldSemi | ensures ( Attribute )* Expression OldSemi | decreases DecreasesList OldSemi ) 
PossiblyWildFrameExpression ::= ( star | FrameExpression ) 
PossiblyWildExpression ::= ( star | Expression ) 
Stmt ::= OneStmt 
ExplicitYieldBlockStmt ::= ( "explicit_yield" | "atomic" ) lbrace ( Stmt )* rbrace 
OneStmt ::= ( BlockStmt | AssertStmt | AssumeStmt | PrintStmt | RevealStmt | SomehowStmt | FenceStmt | GotoStmt | CompareAndSwapStmt | AtomicExchangeStmt | DeallocStmt | CreateThreadStmt | UpdateStmt | VarDeclStatement | IfStmt | WhileStmt | MatchStmt | ForallStmt | CalcStmt | ModifyStmt | "label" LabelIdent colon OneStmt | "break" ( LabelIdent | ( "break" )* ) semi | "continue" semi | ReturnStmt | SkeletonStmt | JoinStmt | ExplicitYieldBlockStmt ) 
AssertStmt ::= "assert" ( Attribute )* ( ( LabelIdent colon )? Expression ( by BlockStmt | semi ) | ellipsis semi ) 
AssumeStmt ::= ( assume | "wait_until" ) ( Attribute )* ( Expression | ellipsis ) semi 
PrintStmt ::= "print" Expression ( comma Expression )* semi 
RevealStmt ::= reveal Expression ( comma Expression )* semi 
SomehowStmt ::= "somehow" ( ( "undefined_unless" Expression ( comma Expression )* | modifies ( Attribute )* Expression ( comma Expression )* | ensures Expression ) )* semi 
FenceStmt ::= "fence" semi 
GotoStmt ::= "goto" LabelIdent semi 
CompareAndSwapStmt ::= "compare_and_swap" openparen Expression comma Expression comma Expression closeparen semi 
AtomicExchangeStmt ::= "atomic_exchange" openparen Expression comma Expression closeparen semi 
DeallocStmt ::= "dealloc" Expression semi 
CreateThreadStmt ::= "create_thread" NoUSIdent openparen ( Expressions )? closeparen semi 
UpdateStmt ::= ( Lhs ( ( Attribute )* semi | ( comma Lhs )* ( ( gets | "::=" ) Rhs ( comma Rhs )* | boredSmiley ( assume )? Expression | ":-" Expression ) semi | colon ) | ":-" Expression semi ) 
VarDeclStatement ::= ( ghost )? ( "noaddr" )? var ( ( Attribute )* LocalIdentTypeOptional ( comma ( Attribute )* LocalIdentTypeOptional )* ( ( ( gets | "::=" ) Rhs ( comma Rhs )* | ( Attribute )* boredSmiley ( assume )? Expression | ":-" Expression ) )? semi | CasePatternLocal ( gets | ( Attribute )* boredSmiley ) Expression semi ) 
IfStmt ::= "if" ( AlternativeBlock | ( ExistentialGuard | Guard | ellipsis ) BlockStmt ( else ( IfStmt | BlockStmt ) )? ) 
WhileStmt ::= "while" ( ( LoopSpec )* AlternativeBlock | ( Guard | ellipsis ) ( LoopSpec )* ( BlockStmt | ellipsis | ) ) 
MatchStmt ::= "match" Expression ( lbrace ( CaseStatement )* rbrace | ( CaseStatement )* ) 
ForallStmt ::= ( "forall" | "parallel" ) ( openparen ( QuantifierDomain )? closeparen | ( QuantifierDomain )? ) ( ( "free" )? ensures Expression OldSemi )* ( BlockStmt )? 
CalcStmt ::= calc ( Attribute )* ( CalcOp )? lbrace ( Expression semi ( CalcOp )? ( ( BlockStmt | CalcStmt ) )* )* rbrace 
ModifyStmt ::= "modify" ( Attribute )* ( FrameExpression ( comma FrameExpression )* | ellipsis ) ( BlockStmt | semi ) 
ReturnStmt ::= ( "return" | "yield" ) ( Rhs ( comma Rhs )* )? semi 
SkeletonStmt ::= ellipsis ( "where" Ident ( comma Ident )* gets Expression ( comma Expression )* )? semi 
JoinStmt ::= "join" Expression semi 
Rhs ::= ( "new" ( NewArray | TypeAndToken ( ( NewArray | openparen ( Expressions )? closeparen ) )? ) | star | Expression | "create_thread" NoUSIdent openparen ( Expressions )? closeparen | "malloc" openparen Type closeparen | "calloc" openparen Type comma Expression closeparen | "compare_and_swap" openparen Expression comma Expression comma Expression closeparen | "atomic_exchange" openparen Expression comma Expression closeparen ) ( Attribute )* 
Lhs ::= ( NameSegment ( Suffix )* | star Expression | ConstAtomExpression Suffix ( Suffix )* ) 
NewArray ::= lbracket ( rbracket lbracket ( Expressions )? rbracket | Expressions rbracket ( ( openparen Expression closeparen | lbracket ( Expressions )? rbracket ) )? ) 
Expressions ::= Expression ( comma Expression )* 
CasePatternLocal ::= ( Ident openparen ( CasePatternLocal ( comma CasePatternLocal )* )? closeparen | openparen ( CasePatternLocal ( comma CasePatternLocal )* )? closeparen | LocalIdentTypeOptional ) 
AlternativeBlock ::= ( lbrace ( AlternativeBlockCase )* rbrace | AlternativeBlockCase ( AlternativeBlockCase )* ) 
ExistentialGuard ::= IdentTypeOptional ( comma IdentTypeOptional )* ( Attribute )* boredSmiley Expression 
Guard ::= ( star | openparen star closeparen | Expression ) 
AlternativeBlockCase ::= case ( ExistentialGuard | Expression ) darrow ( Stmt )* 
LoopSpec ::= ( ( "free" )? invariant ( Attribute )* Expression OldSemi | ensures Expression OldSemi | decreases ( Attribute )* DecreasesList OldSemi | modifies ( Attribute )* FrameExpression ( comma FrameExpression )* OldSemi ) 
CaseStatement ::= case ( Ident ( openparen ( CasePattern ( comma CasePattern )* )? closeparen )? | openparen CasePattern ( comma CasePattern )* closeparen ) darrow ( Stmt )* 
CasePattern ::= ( Ident openparen ( CasePattern ( comma CasePattern )* )? closeparen | openparen ( CasePattern ( comma CasePattern )* )? closeparen | IdentTypeOptional ) 
QuantifierDomain ::= IdentTypeOptional ( comma IdentTypeOptional )* ( Attribute )* ( verticalbar Expression )? 
CalcOp ::= ( eq ( "#" lbracket Expression rbracket )? | openAngleBracket | closeAngleBracket | "<=" | ">=" | neq | neqAlt | "\u2264" | "\u2265" | EquivOp | ImpliesOp | ExpliesOp ) 
EquivOp ::= ( "<==>" | "\u21d4" ) 
ImpliesOp ::= ( "==>" | "\u21d2" ) 
ExpliesOp ::= ( "<==" | "\u21d0" ) 
AndOp ::= ( "&&" | "\u2227" ) 
OrOp ::= ( "||" | "\u2228" ) 
NegOp ::= ( "!" | "\u00ac" ) 
Forall ::= ( "forall" | "\u2200" ) 
Exists ::= ( "exists" | "\u2203" ) 
QSep ::= ( doublecolon | bullet ) 
EquivExpression ::= ImpliesExpliesExpression ( EquivOp ImpliesExpliesExpression )* 
ImpliesExpliesExpression ::= LogicalExpression ( ( ImpliesOp ImpliesExpression | ExpliesOp LogicalExpression ( ExpliesOp LogicalExpression )* ) )? 
LogicalExpression ::= ( AndOp RelationalExpression ( AndOp RelationalExpression )* | OrOp RelationalExpression ( OrOp RelationalExpression )* | RelationalExpression ( ( AndOp RelationalExpression ( AndOp RelationalExpression )* | OrOp RelationalExpression ( OrOp RelationalExpression )* ) )? ) 
ImpliesExpression ::= LogicalExpression ( ImpliesOp ImpliesExpression )? 
RelationalExpression ::= ShiftTerm ( RelOp ShiftTerm ( RelOp ShiftTerm )* )? 
ShiftTerm ::= Term ( ( openAngleBracket openAngleBracket | closeAngleBracket closeAngleBracket ) Term )* 
RelOp ::= ( eq ( "#" lbracket Expression rbracket )? | openAngleBracket | closeAngleBracket | "<=" | ">=" | neq ( "#" lbracket Expression rbracket )? | in | notIn | "!" ( "!" )? | neqAlt | "\u2264" | "\u2265" ) 
Term ::= Factor ( AddOp Factor )* 
Factor ::= BitvectorFactor ( MulOp BitvectorFactor )* 
AddOp ::= ( "+" | "-" ) 
BitvectorFactor ::= AsExpression ( ( "&" AsExpression ( "&" AsExpression )* | verticalbar AsExpression ( verticalbar AsExpression )* | "^" AsExpression ( "^" AsExpression )* ) )? 
MulOp ::= ( star | "/" | "%" ) 
AsExpression ::= UnaryExpression ( as TypeAndToken )* 
UnaryExpression ::= ( "-" UnaryExpression | NegOp UnaryExpression | "&" UnaryExpression | star UnaryExpression | map MapDisplayExpr ( Suffix )* | imap MapDisplayExpr ( Suffix )* | iset ISetDisplayExpr ( Suffix )* | LambdaExpression | EndlessExpression | NameSegment ( Suffix )* | DisplayExpr ( Suffix )* | MultiSetExpr ( Suffix )* | SeqConstructionExpr ( Suffix )* | ConstAtomExpression ( Suffix )* ) 
MapDisplayExpr ::= lbracket ( MapLiteralExpressions )? rbracket 
Suffix ::= ( dot ( openparen MemberBindingUpdate ( comma MemberBindingUpdate )* closeparen | DotSuffix ( GenericInstantiation | HashCall | ) ) | lbracket ( Expression ( ".." ( Expression )? | gets Expression | colon ( Expression ( colon Expression )* ( colon )? )? | ( comma Expression )* ) | ".." ( Expression )? ) rbracket | openparen ( Expressions )? closeparen ) 
ISetDisplayExpr ::= lbrace ( Expressions )? rbrace 
LambdaExpression ::= ( WildIdent | openparen ( IdentTypeOptional ( comma IdentTypeOptional )* )? closeparen ) ( ( reads PossiblyWildFrameExpression ( comma PossiblyWildFrameExpression )* | requires Expression ) )* LambdaArrow Expression 
EndlessExpression ::= ( "if" ( ExistentialGuard | Expression ) then Expression else Expression | MatchExpression | QuantifierGuts | set SetComprehensionExpr | iset SetComprehensionExpr | StmtInExpr Expression | LetExpr | map MapComprehensionExpr | imap MapComprehensionExpr | reveal Expression | NamedExpr ) 
NameSegment ::= Ident ( GenericInstantiation | HashCall | ) 
DisplayExpr ::= ( lbrace ( Expressions )? rbrace | lbracket ( Expressions )? rbracket ) 
MultiSetExpr ::= multiset ( lbrace ( Expressions )? rbrace | openparen Expression closeparen ) 
SeqConstructionExpr ::= seq openparen Expression comma Expression closeparen 
ConstAtomExpression ::= ( "false" | "true" | "null" | Nat | Dec | charToken | stringToken | "this" | "$me" | "$sb_empty" | "$state" | "fresh" openparen Expression closeparen | "allocated" openparen Expression closeparen | "allocated_array" openparen Expression closeparen | "if_undefined" openparen Expression comma Expression closeparen | "global_view" openparen Expression closeparen | "unchanged" ( "@" LabelIdent )? openparen FrameExpression ( comma FrameExpression )* closeparen | "old" ( "@" LabelIdent )? openparen Expression closeparen | verticalbar Expression verticalbar | ( int | real ) openparen Expression closeparen | ParensExpression ) 
Dec ::= decimaldigits 
ParensExpression ::= openparen ( Expressions )? closeparen 
LambdaArrow ::= darrow 
MapLiteralExpressions ::= Expression gets Expression ( comma Expression gets Expression )* 
MapComprehensionExpr ::= IdentTypeOptional ( comma IdentTypeOptional )* ( Attribute )* ( verticalbar Expression )? QSep Expression ( gets Expression )? 
MatchExpression ::= "match" Expression ( lbrace ( CaseExpression )* rbrace | ( CaseExpression )* ) 
QuantifierGuts ::= ( Forall | Exists ) QuantifierDomain QSep Expression 
SetComprehensionExpr ::= IdentTypeOptional ( comma IdentTypeOptional )* ( Attribute )* verticalbar Expression ( QSep Expression )? 
StmtInExpr ::= ( AssertStmt | AssumeStmt | CalcStmt ) 
LetExpr ::= ( LetExprWithLHS | LetExprWithoutLHS ) 
NamedExpr ::= "label" NoUSIdent colon Expression 
LetExprWithLHS ::= ( ghost )? var CasePattern ( comma CasePattern )* ( gets | ( Attribute )* boredSmiley | ":-" ) Expression ( comma Expression )* semi Expression 
LetExprWithoutLHS ::= ":-" Expression semi Expression 
CaseExpression ::= case ( Ident ( openparen ( CasePattern ( comma CasePattern )* )? closeparen )? | openparen CasePattern ( comma CasePattern )* closeparen ) darrow Expression 
HashCall ::= "#" ( GenericInstantiation )? lbracket Expression rbracket openparen ( Expressions )? closeparen 
MemberBindingUpdate ::= ( ident | digits ) gets Expression 
DotSuffix ::= ( ident | digits | decimaldigits | requires | reads ) 

//
// tokens
//

bool ::= "bool"
char ::= "char"
int ::= "int"
nat ::= "nat"
real ::= "real"
ORDINAL ::= "ORDINAL"
object ::= "object"
object_q ::= "object?"
string ::= "string"
set ::= "set"
iset ::= "iset"
multiset ::= "multiset"
seq ::= "seq"
map ::= "map"
imap ::= "imap"
colon ::= ":"
comma ::= ","
verticalbar ::= "|"
doublecolon ::= "::"
gets ::= ":="
boredSmiley ::= ":|"
bullet ::= "\u2022"
dot ::= "."
backtick ::= "`"
semi ::= ";"
darrow ::= "=>"
assume ::= "assume"
calc ::= "calc"
case ::= "case"
then ::= "then"
else ::= "else"
as ::= "as"
by ::= "by"
in ::= "in"
decreases ::= "decreases"
invariant ::= "invariant"
function ::= "function"
predicate ::= "predicate"
inductive ::= "inductive"
twostate ::= "twostate"
copredicate ::= "copredicate"
lemma ::= "lemma"
static ::= "static"
protected ::= "protected"
import ::= "import"
export ::= "export"
class ::= "class"
trait ::= "trait"
datatype ::= "datatype"
codatatype ::= "codatatype"
var ::= "var"
const ::= "const"
newtype ::= "newtype"
type ::= "type"
iterator ::= "iterator"
method ::= "method"
colemma ::= "colemma"
constructor ::= "constructor"
modifies ::= "modifies"
reads ::= "reads"
requires ::= "requires"
ensures ::= "ensures"
ghost ::= "ghost"
witness ::= "witness"
lbracecolon ::= "{:"
lbrace ::= "{"
rbrace ::= "}"
lbracket ::= "["
rbracket ::= "]"
openparen ::= "("
closeparen ::= ")"
openAngleBracket ::= "<"
closeAngleBracket ::= ">"
eq ::= "=="
neq ::= "!="
neqAlt ::= "\u2260"
star ::= "*"
ellipsis ::= "..."
reveal ::= "reveal"
module ::= "module"
commit ::= "commit"

Return more than one value in concrete level

As discussed in the meeting, Armada generates this error for concrete level:

cuckoo.arm_preproc.arm(615,7): Warning: Method cuckoohash_map_lock_three has more than one return value

Here is line 615 of cuckoo.arm_preproc.arm:

method cuckoohash_map_lock_three(this_ptr: ptr<cuckoohash_map>, ...) returns (ret1: TwoBuckets, ret2: LockManager)

Invariant proofs split across files

Proving an invariant sometimes involves two lemmas, one to show that it holds in the initial state and one to show that it's preserved by the next-state relation. Sometimes these two lemmas appear in separate generated files, which is a little odd. It would be more natural for those lemmas to be collocated in the same file.

Regression test framework doesn't support negative examples

We currently use scons scripts as a regression test framework. However, these scripts only support testing that examples are successfully translated, generated, and verified. We don't support testing that an example appropriately fails. It would be useful to have support for checking for proper failures. This would let us, for example, have a regression test that ensures that the compilation checker continues to correctly reject various uncompilable programs.

Dafny uses .expect files to allow this kind of testing. This project should have something similar.

Concrete-level checker unnecessarily rejects return of multiple values

The concrete-level checker rejects a concrete level that contains a method with more than one returned value. However, it doesn't need to do this, since the Clight compiler properly handles returning multiple values.

adding some documentation / samples would be cool

also like a benchmark or something.
how does it perform compared to like http://dotnet.github.io/orleans/ or something.

Empty statement not supported

Armada rejects programs with an empty statement (a bare semicolon). This makes it awkward to write macros, if one is using a preprocessor to generate Armada files.

Can't customize a lemma by removing preconditions

In some cases, a lemma we generate would verify faster if one removed preconditions from it. For instance, if one of the preconditions involves a loosely-triggered quantifier, it might be useful to remove it. So, it may be useful to allow a recipe to specify a lemma customization that, rather than adding material to the body of the proof, instead removes certain specified preconditions.

This issue is a generalization of issue #5, so its solution may also fix that issue.

Can't express well-formedness of an expression

The Armada language doesn't offer a way to describe the conditions under which a certain expression is well-formed. It would be useful to have $wf(E) mean "the expression E is well-formed". For instance, $wf(n/d) would be equivalent to d != 0, and $wf(p + 7) where p is a pointer would be equivalent to "p is a pointer into an array that has at least seven more elements in it beyond p".

Currently, if the developer writes an inductive invariant or yield predicate that isn't always well-formed, we automatically add extra conditions to ensure it's well-formed. For instance, if the developer writes n/d == 3 as an invariant we transform it to d != 0 && n/d == 3. This may be surprising to developers since the invariant we generate doesn't exactly match what they wrote. Providing $wf
in the language might remove the need to change invariants this way.

Pointers to non-heap types don't cause errors

It's not meaningful to declare a pointer to a non-heap type like a datatype, but the parser allows it. It should generate an error.

Some emitted proof elements aren't needed

Sometimes, Armada emits lemmas and/or functions that are never ultimately used by the final proof. This happens because a strategy is generic, and some but not all proofs using that strategy need those elements. The consequence is that the proof takes longer to verify than it needs to.

It would be useful to do a pass over all the elements before emitting them to remove any that aren't needed.