Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Removed code related to "divided" option. | 2012-08-13 | |
| | |||
* | Barrier divergence checking now achieved via precondition. | 2012-08-13 | |
| | | | | | | Race checking assertions contain tags to identify them. Attributes are passed correctly through the dualisation process. | ||
* | Unstructured and smart predication are now default options for GPUVerify. | 2012-08-09 | |
| | | | | | | The executable produced by building the project is now GPUVerifyVCGen. Refactored the way "other" functions are handled to make this more easily extensible. | ||
* | Revised candidate invariant generation for barrier divergence checking. | 2012-08-07 | |
| | |||
* | Smart block predicator: drop the unused createCandidateInvariants parameter | 2012-08-06 | |
| | |||
* | GPUVerify: add an option which controls whether to use smart predication | 2012-07-30 | |
| | |||
* | Implemented Houdini-based pointer analysis. Made inter-group race checking ↵ | 2012-07-20 | |
| | | | | default. | ||
* | GPUVerify only generates _READ/WRITE_OFFSET variabls if they do not already ↵ | 2012-07-17 | |
| | | | | exist. Did some tidying up of old source code - removed functions related to Y and Z offsets which we do not use any more. | ||
* | Merge | 2012-07-10 | |
|\ | |||
* | | Read and write logging variables are now only generated if they do not ↵ | 2012-07-10 | |
| | | | | | | | | already exist. | ||
| * | GPUVerify: merge blocks into predecessors before and after predication | 2012-07-09 | |
|/ | | | | | | | Because predication produces straight line control flow, merging after predication can dramatically reduce the number of blocks to 1 plus 2-3 per loop. We also merge before predication, which reduces VC complexity by reducing the number of possible values for cur. | ||
* | Worked on cross-thread annotations. | 2012-07-03 | |
| | |||
* | Reinstate GPUVerify files | 2012-07-02 | |
| | |||
* | Merge | 2012-07-02 | |
|\ | |||
* | | Started adding support for annotation intrinsics for unstructured programs. | 2012-07-02 | |
| | | |||
| * | Merge | 2012-06-28 | |
| |\ | |/ |/| | |||
| * | Dafny: Merge | 2012-06-27 | |
| |\ | |||
* | | | GPUVerify: modify the variable definition analysis to track and reject ↵ | 2012-06-27 | |
| |/ |/| | | | | | | | | | self-referential definitions Fixes Bugzilla bug #66. | ||
* | | GPUVerify: when building offset predicates, skip unsubstitutable offsets | 2012-06-27 | |
| | | | | | | | | Fixes Bugzilla bug #65. | ||
* | | GPUVerify: use original expression for undefined variables | 2012-06-27 | |
| | | | | | | | | Fixes Bugzilla bug #64. | ||
* | | GPUVerify: implement generic reduced strength analysis for loop counters | 2012-06-26 | |
| | | | | | | | | | | | | | | | | | | | | All counters which we are able to infer facts about now receive a candidate invariant _before_ predication, dualisation etc. This is probably a more natural place to insert such invariants, and means that they are also subject to predication etc. without us having to do anything. Also, kill the id plus constant analyses, which are no longer used. | ||
* | | GPUVerify: fix UnstructuredRegion.CmdsChildRegions | 2012-06-26 | |
| | | |||
* | | Reinstated support for barrier flags. | 2012-06-27 | |
| | | |||
* | | Undo bad merge. | 2012-06-27 | |
| | | |||
* | | Merge | 2012-06-26 | |
|\ \ | |||
* | | | Added support for barrier flags. | 2012-06-26 | |
| | | | |||
* | | | Merge | 2012-06-25 | |
|\ \ \ | |||
| | * | | GPUVerify: factor all offset predicate handling code into a central location | 2012-06-25 | |
| | | | | |||
| | * | | GPUVerify: merge ElementEncodingRaceInstrumenter into RaceInstrumenter | 2012-06-22 | |
| |/ / | |||
| * | | GPUVerify: implement generic stride constraint generation | 2012-06-22 | |
| | | | |||
| * | | GPUVerify: make VarDefAnalysis capable of analysing non-constants | 2012-06-22 | |
| | | | |||
| * | | GPUVerify: construct BV*_AND and BV*_SUB using MakeBVFunctionCall | 2012-06-21 | |
| | | | |||
| * | | GPUVerify: replace MayBe{ThreadConfigurationVariable,Gid}Analyser with ↵ | 2012-06-21 | |
| | | | | | | | | | | | | | | | | | | | | | simple functions based on VariableDefinitionAnalysis This also unbreaks the stride race instrumentation for various subtle reasons. | ||
* | | | Merge | 2012-06-21 | |
|\ \ \ | |||
| | * | | GPUVerify: make BuildNamedDefVisitor and SubstDualisedDefVisitor Duplicators | 2012-06-20 | |
| |/ / | |||
| * / | GPUVerify: fix constant offset invariant generation for the case where no ↵ | 2012-06-20 | |
| |/ | | | | | | | constants are found | ||
| * | Move block predicator to VCGeneration | 2012-06-18 | |
| | | |||
| * | GPUVerify: block predicator: add a mode which disables procedure predicates | 2012-06-18 | |
| | | | | | | | | | | This mode also conditionalises if statements to avoid problems with recursion. | ||
* | | Merge with dafny_runtime_checking | 2012-06-18 | |
|\| | |||
* | | Added command line option. | 2012-06-18 | |
| | | |||
| * | GPUVerify: implement is-a-constant analysis | 2012-06-15 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | This analysis is used to generate race checking invariants for arbitrary (thread-level) constant offsets, in place of invariant generators for four specific constants (thread-id, global-id, 2D thread-id and 2D global-id) which are subsumed by the new analysis. The main motivation is to be able to recognise offsets used by word level accesses into byte arrays, which are formed from linear combinations of thread IDs and constants. This change allows us to remove the 2D and global size analyses, resulting in a 536-line net reduction in total code size. | ||
| * | GPUVerify: revert ac36537a0eb8, as this is in fact a candidate invariant ↵ | 2012-06-15 | |
| | | | | | | | | | | | | (e.g. consider a loop within a conditional) Pointed out by Ally. | ||
| * | GPUVerify: when dualising assume and assert statements, emit two statements ↵ | 2012-06-15 | |
|/ | | | | instead of a conjunction | ||
* | Inter-thread race checking implementation done. | 2012-06-14 | |
| | |||
* | Fix for structured regions. | 2012-06-14 | |
| | |||
* | Progress on inter-group race checking | 2012-06-14 | |
| | |||
* | Merge | 2012-06-14 | |
|\ | |||
* | | Started work on inter-group race checking. | 2012-06-14 | |
| | | |||
| * | GPUVerify: the non-uniform loop invariant is not a candidate invariant | 2012-06-12 | |
| | | | | | | | | Thanks to Ally for pointing this out. | ||
| * | GPUVerify: emit non-uniform loop candidate invariant | 2012-06-11 | |
| | |