summaryrefslogtreecommitdiff
path: root/Source/GPUVerify
Commit message (Expand)AuthorAge
* Fixed bug with uniformity analysis for havoc. Allowed barrier invariants toGravatar Unknown2012-09-28
* Barrier invariants can now refer to local variables that are uniform.Gravatar Unknown2012-09-26
* Fixed issue with uniformity analysis and block merging. Uniformity analysisGravatar Unknown2012-09-24
* Support for barrier invariants.Gravatar Unknown2012-09-24
* Fixed a bug with empty big blocks.Gravatar Unknown2012-09-21
* Added support for invariants about shared state.Gravatar Unknown2012-09-21
* When uniformity analysis is disabled, no procedures (even the kernel entryGravatar Unknown2012-09-19
* Uniformity analysis. Patch by Peter Collingbourne.Gravatar Unknown2012-09-18
* Dualisation modified so that global arrays are not dualised, and group-sharedGravatar Unknown2012-09-18
* During dualisation,Gravatar Unknown2012-09-17
* Added creation of source variable pre- and post- conditions.Gravatar Egor Kyshtymov2012-09-16
* Moved point at which preprocessed output is shown.Gravatar Unknown2012-08-31
* Shared state is now properly abstracted in requires clauses.Gravatar Unknown2012-08-31
* Barriers now handled uniformly via bugle_barrier.Gravatar Unknown2012-08-30
* A small fix in variable definition analysis.Gravatar Unknown2012-08-29
* Added generation of invariants to restrict source location to sensible values.Gravatar Egor Kyshtymov2012-08-28
* Fixed problem where SOURCE variables were not being generated.Gravatar Unknown2012-08-20
* Added functionality for race error reporting.Gravatar Egor Kyshtymov2012-08-20
* Fixed bug where source location attributes are not being attached to a CHECKGravatar Unknown2012-08-16
* Separated race checking into logging and checking calls. This simplifiesGravatar Unknown2012-08-14
* Removed some dud code for handling nested maps, which we no longer support.Gravatar Unknown2012-08-13
* Some more code cleanup related to removal of the "divided" option.Gravatar Unknown2012-08-13
* Removed code related to "divided" option.Gravatar Unknown2012-08-13
* Barrier divergence checking now achieved via precondition.Gravatar Unknown2012-08-13
* Unstructured and smart predication are now default options for GPUVerify.Gravatar Unknown2012-08-09
* Revised candidate invariant generation for barrier divergence checking.Gravatar Unknown2012-08-07
* Smart block predicator: drop the unused createCandidateInvariants parameterGravatar Peter Collingbourne2012-08-06
* GPUVerify: add an option which controls whether to use smart predicationGravatar Peter Collingbourne2012-07-30
* Implemented Houdini-based pointer analysis. Made inter-group race checking d...Gravatar Unknown2012-07-20
* GPUVerify only generates _READ/WRITE_OFFSET variabls if they do not already e...Gravatar Unknown2012-07-17
* MergeGravatar Unknown2012-07-10
|\
* | Read and write logging variables are now only generated if they do not alread...Gravatar Unknown2012-07-10
| * GPUVerify: merge blocks into predecessors before and after predicationGravatar Peter Collingbourne2012-07-09
|/
* Worked on cross-thread annotations.Gravatar Unknown2012-07-03
* Reinstate GPUVerify filesGravatar Peter Collingbourne2012-07-02
* MergeGravatar Unknown2012-07-02
|\
* | Started adding support for annotation intrinsics for unstructured programs.Gravatar Unknown2012-07-02
| * MergeGravatar Jason Koenig2012-06-28
| |\ | |/ |/|
| * Dafny: MergeGravatar Jason Koenig2012-06-27
| |\
* | | GPUVerify: modify the variable definition analysis to track and reject self-r...Gravatar Peter Collingbourne2012-06-27
| |/ |/|
* | GPUVerify: when building offset predicates, skip unsubstitutable offsetsGravatar Peter Collingbourne2012-06-27
* | GPUVerify: use original expression for undefined variablesGravatar Peter Collingbourne2012-06-27
* | GPUVerify: implement generic reduced strength analysis for loop countersGravatar Peter Collingbourne2012-06-26
* | GPUVerify: fix UnstructuredRegion.CmdsChildRegionsGravatar Peter Collingbourne2012-06-26
* | Reinstated support for barrier flags.Gravatar Unknown2012-06-27
* | Undo bad merge.Gravatar afd2012-06-27
* | MergeGravatar Unknown2012-06-26
|\ \
* | | Added support for barrier flags.Gravatar Unknown2012-06-26
* | | MergeGravatar Unknown2012-06-25
|\ \ \
| | * | GPUVerify: factor all offset predicate handling code into a central locationGravatar Peter Collingbourne2012-06-25