课题基金 / 基金详情

SHF: Small: Specifying and Verifying Essential Deterministic Behavior of Concurrent Programs

SHF: Small: Specifying and Verifying Essential Deterministic Behavior of Concurrent Programs
SHF:小:指定和验证并发程序的基本确定性行为
批准号:
1018730
负责人:
Koushik Sen
金额:
$47.54万
依托单位国家:
美国
项目类别:
Standard Grant
财政年份:
2010
资助国家:
美国
项目状态:
已结题
起止时间:
2010-08-01 至 2015-07-31

项目摘要

项目成果

Koushik Sen的其他基金

相似基金

相关文献

中文摘要
翻译
并行多线程程序比它们的顺序程序更难编写,因为在编写并行程序时,程序员除了考虑程序的算法正确性外,还必须考虑由于线程交错而导致的所有可能的行为。一个普遍的信念是,使大量程序员能够访问多线程编程的唯一方法是提出编程范例和相关工具,明确地将关于函数正确性的推理与关于由并行引起的额外行为的推理分开。该项目研究将程序的并行化正确性方面与其函数正确性分离的策略。首先,对于大多数并行程序来说,希望由并行程序中的线程调度器引入的不确定性不会改变程序的预期输出。这个项目将开发一个断言框架,用于指定并行程序的区域在非确定性线程交织的情况下具有确定性的行为。第二种策略基于这样的观察,即并行程序开发的一个自然步骤是首先使用受控的非确定性扩展顺序算法,然后在线程交织引入额外的不确定性时进行实际的并行化。这个项目将研究非确定性顺序程序作为一种规范机制的使用,使得对于并行程序的每次执行,存在对应的非确定性顺序程序的等价执行。这种不确定的顺序程序将并行化正确性与功能正确性解耦。
英文摘要
Parallel multi-threaded programs are more difficult to write than their sequential counterparts because while writing parallel programs programmers must consider all possible behaviors due to thread interleavings, in addition to the algorithmic correctness of the program. A widespread belief is that the only way to make multi-threaded programming accessible to a large number of programmers is to come up with programming paradigms and associated tools that explicitly separate reasoning about functional correctness from reasoning about additional behaviors arising due to parallelism.This project investigates strategies for separating the parallelization correctness aspect of a program from its functional correctness. First, for most parallel programs it is desired that the non-determinism introduced by the thread scheduler in a parallel program does not change the intended output of the program. This project will develop an assertion framework for specifying that regions of a parallel program behave deterministically despite non-deterministic thread interleaving.The second strategy is based on the observation that a natural step in the development of a parallel program is to first extend the sequential algorithm with a controlled amount of non-determinism, followed by the actual parallelization, when additional non-determinism is introduced by thread interleavings. This project will investigate the use of non-deterministic sequential programs as a specification mechanism, such that for each execution of a parallel program there exists an equivalent execution of the corresponding non-deterministic sequential program. Such non-deterministic sequential programs decouple parallelization correctness from functional correctness.
期刊论文(0)
专著(0)
科研奖励(0)
会议论文
SHF: Small: Automatic Exploration and Analysis of Software Performance Responses
  • 批准号:
    1908870
  • 项目类别:
    Standard Grant
  • 资助金额:
    $50.0万
  • 财政年份:
    2019
  • 负责人:
    Koushik Sen
  • 依托单位:
SHF: Medium: Collaborative Research: HUGS: Human-Guided Software Testing and Analysis for Scalable Bug Detection and Repair
  • 批准号:
    1900968
  • 项目类别:
    Continuing Grant
  • 资助金额:
    $40.0万
  • 财政年份:
    2019
  • 负责人:
    Koushik Sen
  • 依托单位:
SaTC: CORE: Small: Machine Learning for Effective Fuzz Testing
  • 批准号:
    1817122
  • 项目类别:
    Standard Grant
  • 资助金额:
    $50.0万
  • 财政年份:
    2018
  • 负责人:
    Koushik Sen
  • 依托单位:
SHF: Medium: Automated Graphical User Interface Testing with Learning
  • 批准号:
    1409872
  • 项目类别:
    Standard Grant
  • 资助金额:
    $85.0万
  • 财政年份:
    2014
  • 负责人:
    Koushik Sen
  • 依托单位:
国内基金
海外基金
昼夜节律性small RNA在血斑形成时间推断中的法医学应用研究
  • 批准号:
  • 项目类别:
    省市级项目
  • 资助金额:
    --
  • 批准年份:
    2024
  • 负责人:
  • 依托单位:
tRNA-derived small RNA上调YBX1/CCL5通路参与硼替佐米诱导慢性疼痛的机制研究
  • 批准号:
  • 项目类别:
    省市级项目
  • 资助金额:
    10.0万元
  • 批准年份:
    2022
  • 负责人:
    张祥忠
  • 依托单位:
Small RNA调控I-F型CRISPR-Cas适应性免疫性的应答及分子机制
Small RNAs调控解淀粉芽胞杆菌FZB42生防功能的机制研究
  • 批准号:
    31972324
  • 项目类别:
    面上项目
  • 资助金额:
    58.0万元
  • 批准年份:
    2019
  • 负责人:
    高学文
  • 依托单位: