相关实验视频
通过注释意识的转换来保护GPU程序优化的可证明性
Ömer Şakar1, Mohsen Safari2, Marieke Huisman1
1Formal Methods and Tools, University of Twente, Enschede, The Netherlands.
概括
本研究介绍了注释意识的转换,以自动优化GPU程序. 这种方法可以保持代码的正确性,并为开发人员简化验证过程.
科学领域:
- 计算机科学 计算机科学
- 软件工程 软件工程 软件工程
- 高性能计算 高性能计算
背景情况:
- GPU程序需要手动优化性能,这可能会引入错误.
- 标注 (前后条件) 捕捉功能性质,但在优化过程中很难保持.
研究的目的:
- 提出一种自动优化GPU程序的方法,同时保持其可证明性.
- 引入注释意识的转换,修改代码和注释.
主要方法:
- 开发了注释意识的转换来应用GPU优化.
- 在Alpinist工具中实现了该方法.
- 在经过验证的程序上使用VerCors程序验证器对Alpinist进行评估.
主要成果:
- 证明了对GPU程序自动应用优化的能力.
- 展示了通过转换的注释来保存可证明性的方法.
- 使用Alpinist和VerCors.成功地重新验证了优化的程序.
结论:
- 注释意识转换为优化GPU程序提供了一个自动化解决方案.
- 这种方法减少了与手动优化和注释维护相关的劳动和错误易感.
- 阿尔卑斯人促进了正确和高性能GPU软件的开发.
相关概念视频
Improving Translational Accuracy
14.0K
Base complementarity between the three base pairs of mRNA codon and the tRNA anticodon is not a failsafe mechanism. Inaccuracies can range from a single mismatch to no correct base pairing at all. The free energy difference between the correct and nearly correct base pairs can be as small as 3 kcal/ mol. With complementarity being the only proofreading step, the estimated error frequency would be one wrong amino acid in every 100 amino acids incorporated. However, error frequencies observed in...
14.0K
Improving Translational Accuracy
3.5K
3.5K
Transformations of Functions III
149
Transformations modify the graphical representation of a function without changing its fundamental form. One common transformation is reflection, which flips the graph across a designated axis. When the vertical coordinates of all points are multiplied by the negative one, the entire graph is mirrored over the horizontal axis. This transformation reverses the vertical orientation of peaks and troughs, akin to signal inversion in electrical systems, where a waveform is flipped, but the timing of...
149
Transformations of Functions II
124
Transformations in mathematics alter the position or orientation of a function’s graph while preserving its fundamental shape. One important type of transformation is the horizontal shift, which involves modifying the input variable within a function’s equation. This operation affects where outputs occur along the horizontal axis but does not alter the function’s overall structure.A horizontal shift is achieved by replacing the input variable x with either x + c or x - c,...
124
Statically Indeterminate Problem Solving
670
Statically indeterminate problems are those where statics alone can not determine the internal forces or reactions. Consider a structure comprising two cylindrical rods made of steel and brass. These rods are joined at point B and restrained by rigid supports at points A and C. Now, the reactions at points A and C and the deflection at point B are to be determined. This rod structure is classified as statically indeterminate as the structure has more supports than are necessary for maintaining...
670
Parallel Processing
605
The brain processes sensory information rapidly due to parallel processing, which involves sending data across multiple neural pathways at the same time. This method allows the brain to manage various sensory qualities, such as shapes, colors, movements, and locations, all concurrently. For instance, when observing a forest landscape, the brain simultaneously processes the movement of leaves, the shapes of trees, the depth between them, and the various shades of green. This enables a quick and...
605