summaryrefslogtreecommitdiff
path: root/Source/Concurrency
Commit message (Collapse)AuthorAge
* Rename DLLs to non-generic names by prefixing "Boogie". Project names andGravatar akashlal2016-04-15
| | | | namespaces remain the same.
* bug fix in the type checking of calls to atomic proceduresGravatar Shaz Qadeer2015-10-16
|
* bug fixGravatar Shaz Qadeer2015-10-09
|
* removed an extraneous warningGravatar Shaz Qadeer2015-10-08
|
* added a fix to check all layers: created layer of actions or layers inGravatar Shaz Qadeer2015-10-01
| | | | requires, ensures, or asserts
* another fix requested by ChrisGravatar Shaz Qadeer2015-10-01
| | | | verification is performed now for all created layers
* cleaned up some namesGravatar Shaz Qadeer2015-09-28
|
* a bug fixGravatar Shaz Qadeer2015-09-27
|
* fixed a small bugGravatar Shaz Qadeer2015-09-27
|
* removed a warningGravatar Shaz Qadeer2015-09-26
|
* added introduced and ghost local variablesGravatar Shaz Qadeer2015-09-25
|
* fixed my earlier to make it nicerGravatar Shaz Qadeer2015-09-03
|
* fixed a crash when there is no collectorGravatar Shaz Qadeer2015-09-02
|
* Normalise line endings using a .gitattributes file. UnfortunatelyGravatar Dan Liew2015-06-28
| | | | | | this required that this commit globally modify most files. If you want to use git blame to see the real author of a line use the ``-w`` flag so that whitespace changes are ignored.
* modified desugaring so that in commutatitivity checks copies of originalGravatar qadeer2015-06-17
| | | | codeexpr is made.
* relaxed the check for created and hidden layers for skip actionsGravatar qadeer2015-06-10
|
* fixed crashGravatar qadeer2015-06-10
|
* added assume about gate after calls and parallel callsGravatar qadeer2015-05-31
|
* patched ghost checkingGravatar qadeer2015-04-18
|
* changed aux attribute to ghostGravatar qadeer2015-04-18
|
* fixed the treatment of externGravatar qadeer2015-04-17
|
* patched the type checker to deal with modularityGravatar qadeer2015-04-16
|
* removed "layer" attribute from the desugared programGravatar qadeer2015-01-16
|
* strengthened type checkingGravatar qadeer2014-12-26
| | | | | cleaned up the generation of mover checks (based on example from Chris) added two examples from Chris to regressions
* changed type checking of yield procedures so that they can only call other ↵Gravatar qadeer2014-12-18
| | | | yielding procedures
* some refactoring to separate the concept of shared variables under ↵Gravatar qadeer2014-12-17
| | | | refinement checking with all global variables
* patched last check inGravatar qadeer2014-12-15
|
* 1. made variable introduction layer explicit in the test casesGravatar qadeer2014-12-15
| | | | 2. if a single layer is specified for a global variable, that layer is the introduction layer
* systematic renaming of phase to layerGravatar qadeer2014-12-15
|
* fixed bug due to incomplete erasure of :linear attributeGravatar qadeer2014-12-05
|
* renamed :phase to :layerGravatar qadeer2014-11-14
|
* a fix to type checkingGravatar qadeer2014-11-09
|
* MergeGravatar qadeer2014-10-14
|\
* | reversed the order of generated procedures; commutativity checks are ↵Gravatar qadeer2014-10-14
| | | | | | | | generated first
| * Fix bug in Duplicator where GotoCmd's LabelTargets and LabelNamesGravatar Dan Liew2014-10-05
|/ | | | | | | | | | | where not updated during duplication to point to duplicated BasicBlocks. Because the lists weren't being duplicated and resolved to the new basic blocks a duplicated Implementation pointed into Blocks in the old implementation via GotoCmds. This is bad and is not the expected behaviour. Now if VisitImplementation() is called during duplication GotoCmds will be resolved to point to duplicated Blocks.
* Did more refactoring and addressed several todos.Gravatar wuestholz2014-09-23
|
* Did more refactoring.Gravatar wuestholz2014-09-23
|
* Did some refactoring.Gravatar wuestholz2014-09-23
|
* deleted the free assume about gates after parallel callsGravatar qadeer2014-07-26
|
* enabled merging of yield callsGravatar qadeer2014-07-20
|
* added support for facoring out calls to yield checkers; this will help avoid ↵Gravatar qadeer2014-07-20
| | | | quadratic space complexity
* updated the linear type system based on Chris' design with linear, ↵Gravatar qadeer2014-07-15
| | | | linear_in, linear_out
* fixed a regression failureGravatar qadeer2014-07-15
|
* simplified yield type chcking and added treiber stack (not fully done)Gravatar qadeer2014-07-15
|
* fixed some tests in ogGravatar qadeer2014-07-11
| | | | | added another test in linear (based on bug reported by Chris) removed the QED build configuration
* various fixesGravatar qadeer2014-06-02
|
* a small fixGravatar qadeer2014-05-21
|
* a bug fixGravatar qadeer2014-05-07
|
* added {:aux} attribute to local variablesGravatar qadeer2014-05-07
|
* third checkpoint (refactored more code)Gravatar qadeer2014-05-05
|