检索结果-内蒙古大学图书馆

An Integration of Several Different data flow analysis Techniques

学校读者我要写书评

暂无评论

An Integration of Several Different Data Flow Analysis Techn...

International Conference on Trustworthy Computing and Services, ISCTCS 2012

作者： Xing, Yuchen Wang, Hanfei Zhao, Jianhua Department of Computer Science and Technology Nanjing University Nanjing China

ISBN: (纸本)9783642357947

This paper describes a tool which integrates three different kinds of data flow analysis techniques: null pointer dereference analysis, integer variables differences analysis and single linked list analysis. Each one of them can share and exchange program information with the other two. And also users can add properties manually to enhance the processing capabilities. Through the demonstration in the case study section, we can see that our tool achieves the goal to connect these three analysis techniques and can explore more insightful program information with the artificial help. © Springer-Verlag Berlin Heidelberg 2013.

关键词： data flow analysis

Failure Transparency in Stateful dataflow Systems (Technical Report)

学校读者我要写书评

暂无评论

arXiv 2024年

作者： Veresov, Aleksey Spenger, Jonas Carbone, Paris Haller, Philipp EECS and Digital Futures KTH Royal Institute of Technology Stockholm Sweden Digital Systems RISE Research Institutes of Sweden Stockholm Sweden

Failure transparency enables users to reason about distributed systems at a higher level of abstraction, where complex failure-handling logic is hidden. This is especially true for stateful dataflow systems, which are the backbone of many cloud applications. In particular, this paper focuses on proving failure transparency in Apache Flink, a popular stateful dataflow system. Even though failure transparency is a critical aspect of Apache Flink, to date it has not been formally proven. Showing that the failure transparency mechanism is correct, however, is challenging due to the complexity of the mechanism itself. Nevertheless, this complexity can be effectively hidden behind a failure transparent programming interface. To show that Apache Flink is failure transparent, we model it in small-step operational semantics. Next, we provide a novel definition of failure transparency based on observational explainability, a concept which relates executions according to their observations. Finally, we provide a formal proof of failure transparency for the implementation model;i.e., we prove that the failure-free model correctly abstracts from the failure-related details of the implementation model. We also show liveness of the implementation model under a fair execution assumption. These results are a first step towards a verified stack for stateful dataflow systems. © 2024, CC BY.

关键词： data flow analysis

LoopSCC: Towards Summarizing Multi-branch Loops within Determinate Cycles

学校读者我要写书评

暂无评论

arXiv 2024年

作者： Zhu, Kai Guo, Chenkai Yan, Kuihao Jia, Xiaoqi Du, Haichao Huang, Qingjia Xie, Yamin Tang, Jing Institute of Information Engineering China Nankai University China

Analyzing programs with loops is a challenging task, suffering from potential issues such as indeterminate number of iterations and exponential growth of control flow complexity. Loop summarization, as a static analysis method for concrete semantic interpretation, receives increasing focuses in the field of loop program analysis. By analyzing and representing the regularity in loop control flow, it produces symbolic expressions semantically equivalent to the loop program, enhancing the accuracy and efficiency of loop analysis. However, current loop summarization methods are only suitable for single-branch loops or multi-branch loops with simple cycles, without supporting complex loops with irregular branch-to-branch transitions. In this paper, we proposed LoopSCC, a novel loop summarization technique, to achieve concrete semantic interpretation on complex loop control flow. LoopSCC first utilizes an inside-out transformation to convert the nested loop into non-nested one. Then, it analyzes the control flow at the granularity of single-loop-path and applies the strongly connected components (SCC for short) for contraction and simplification, resulting in the contracted single-loop-path graph (CSG for short). Based on the control flow information provided by the CSG, we can convert the loop summary into a combination of SCC summaries. When an SCC contains irregular branch-to-branch transitions, we propose to explore a convergent range to identify the determinate cycles of different execution paths, referred as oscillatory interval. According to the analysis of oscillatory interval, the loop summarization composed of both iteration conditions and execution operations can eventually be derived recursively. Extensive experiments compared to six state-of-the-art loop interpretation methods are conducted to evaluate the effectiveness of LoopSCC. From the results, LoopSCC outperforms comparative methods in both interpretation accuracy and application effectiveness. Especial

关键词： data flow analysis

LLMDFA: Analyzing dataflow in Code with Large Language Models

学校读者我要写书评

暂无评论

arXiv 2024年

作者： Wang, Chengpeng Zhang, Wuqi Su, Zian Xu, Xiangzhe Xie, Xiaoheng Zhang, Xiangyu Purdue University United States Hong Kong University of Science and Technology Hong Kong Ant Group China

MSC Codes 68N30, 68T01dataflow analysis is a fundamental code analysis technique that identifies dependencies between program values. Traditional approaches typically necessitate successful compilation and expert customization, hindering their applicability and usability for analyzing uncompilable programs with evolving analysis needs in real-world scenarios. This paper presents LLMDFA, an LLM-powered compilation-free and customizable dataflow analysis framework. To address hallucinations for reliable results, we decompose the problem into several subtasks and introduce a series of novel strategies. Specifically, we leverage LLMs to synthesize code that outsources delicate reasoning to external expert tools, such as using a parsing library to extract program values of interest and invoking an automated theorem prover to validate path feasibility. Additionally, we adopt a few-shot chain-of-thought prompting to summarize dataflow facts in individual functions, aligning the LLMs with the program semantics of small code snippets to mitigate hallucinations. We evaluate LLMDFA on synthetic programs to detect three representative types of bugs and on real-world Android applications for customized bug detection. On average, LLMDFA achieves 87.10% precision and 80.77% recall, surpassing existing techniques with F1 score improvements of up to 0.35. We have open-sourced LLMDFA at https://***/chengpeng-wang/LLMDFA. © 2024, CC BY.

关键词： data flow analysis

Bayesian inference using data flow analysis 2013

学校读者我要写书评

暂无评论

Bayesian inference using data flow analysis

2013 9th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering, ESEC/FSE 2013

作者： Claret, Guillaume Rajamani, Sriram K. Nori, Aditya V. Gordon, Andrew D. Borgström, Johannes INRIA France Microsoft Research India Microsoft Research Cambridge United Kingdom Uppsala University Sweden

ISBN: (纸本)9781450322379

We present a new algorithm for Bayesian inference over probabilistic programs, based on data flow analysis techniques from the program analysis community. Unlike existing techniques for Bayesian inference on probabilistic programs, our data flow analysis algorithm is able to perform inference directly on probabilistic programs with loops. Even for loop-free programs, we show that data flow analysis offers better precision and better performance benefits over existing techniques. We also describe heuristics that are crucial for our inference to scale, and present an empirical evaluation of our algorithm over a range of benchmarks. Copyright 2013 ACM.

关键词： data flow analysis

MR-Adopt: Automatic Deduction of Input Transformation Function for Metamorphic Testing

学校读者我要写书评

暂无评论

arXiv 2024年

作者： Xu, Congying Chen, Songqiang Wu, Jiarong Cheung, Shing-Chi Terragni, Valerio Zhu, Hengcheng Cao, Jialun The Hong Kong University of Science and Technology Hong Kong Guangzhou HKUST Fok Ying Tung Research Institute China The University of Auckland Auckland New Zealand

While a recent study reveals that many developer-written test cases can encode a reusable Metamorphic Relation (MR), over 70% of them directly hard-code the source input and follow-up input in the encoded relation. Such encoded MRs, which do not contain an explicit input transformation to transform the source inputs to corresponding follow-up inputs, cannot be reused with new source inputs to enhance test adequacy. In this paper, we propose MR-Adopt (Automatic Deduction Of inPut Transformation) to automatically deduce the input transformation from the hard-coded source and follow-up inputs, aiming to enable the encoded MRs to be reused with new source inputs. With typically only one pair of source and follow-up inputs available in an MR-encoded test case as the example, we leveraged LLMs to understand the intention of the test case and generate additional examples of source-followup input pairs. This helps to guide the generation of input transformations generalizable to multiple source inputs. Besides, to mitigate the issue that LLMs generate erroneous code, we refine LLM-generated transformations by removing MR-irrelevant code elements with data-flow analysis. Finally, we assess candidate transformations based on encoded output relations and select the best transformation as the result. Evaluation results show that MR-Adopt can generate input transformations applicable to all experimental source inputs for 72.00% of encoded MRs, which is 33.33% more than using vanilla GPT-3.5. By incorporating MR-Adopt-generated input transformations, encoded MR-based test cases can effectively enhance the test adequacy, increasing the line coverage and mutation score by 10.62% and 18.91%, respectively. © 2024, CC BY.

关键词： data flow analysis

OpenMP aware MHP analysis for improved static data-race detection

学校读者我要写书评

暂无评论

arXiv 2021年

作者： Bora, Utpal Vaishay, Shraiysh Joshi, Saurabh Upadrasta, Ramakrishna Computer Science and Engineering Indian Institute of Technology Hyderabad India

data races, a major source of bugs in concurrent programs, can result in loss of manpower and time as well as data loss due to system failures. OpenMP, the de facto shared memory parallelism framework used in the HPC community, also suffers from data races. To detect race conditions in OpenMP programs and improve turnaround time and/or developer productivity, we present a data flow analysis based, fast, static data race checker in the LLVM compiler framework. Our tool can detect races in the presence or absence of explicit barriers, with implicit or explicit synchronization. In addition, our tool effectively works for the OpenMP target offloading constructs and also supports the frequently used OpenMP constructs. We formalize and provide a data flow analysis framework to perform Phase Interval analysis (PIA) of OpenMP programs. Phase intervals are then used to compute the MHP (and its complement NHP) sets for the programs, which, in turn, are used to detect data races statically. We evaluate our work using multiple OpenMP race detection benchmarks and real world applications. Our experiments show that the checker is comparable to the state-of-the-art in various performance metrics with around 90% accuracy, almost perfect recall, and significantly lower runtime and memory footprint. © 2021, CC BY-NC-SA.

关键词： data flow analysis

Rely/Guarantee Reasoning for Multicopy Atomic Weak Memory Models 24th

学校读者我要写书评

暂无评论

Rely/Guarantee Reasoning for Multicopy Atomic Weak Memory Mo...

24th International Symposium on Formal Methods (FM)

作者： Coughlin, Nicholas Winter, Kirsten Smith, Graeme Def Sci & Technol Grp Brisbane Qld Australia Univ Queensland Sch Informat Technol & Elect Engn Brisbane Qld Australia

ISBN: (纸本)9783030908706;9783030908690

Rely/guarantee reasoning provides a compositional approach to reasoning about concurrent programs. However, such reasoning traditionally assumes a sequentially consistent memory model and hence is unsound on modern hardware in the presence of data races. In this paper, we present a rely/guarantee-based approach for multicopy atomic weak memory models, i.e., where a thread's stores become observable to all other threads at the same time. Such memory models include those of the widely used x86-TSO and ARMv8 processor architectures, as well as the open-source RISC-V architecture. In this context, an operational semantics can be based on thread-local instruction reordering. We exploit this to provide an efficient compositional proof technique in which weak memory behaviour can be shown to preserve rely/guarantee reasoning on a sequentially consistent memory model. To achieve this, we introduce a side-condition, reordering interference freedom, reducing the complexity of weak memory to checks over pairs of reorderable instructions. To enable practical application, we also define a dataflow analysis capable of identifying a thread's reorderable instructions. All aspects of our approach have been encoded and proved sound in Isabelle/HOL.

关键词： data flow analysis

Interprocedural data flow analysis in soot using value contexts

学校读者我要写书评

暂无评论

Interprocedural data flow analysis in soot using value conte...

2nd ACM SIGPLAN International Workshop on State of the Art in Java Program analysis, SOAP 2013

作者： Padhye, Rohan Khedker, Uday P. Indian Institute of Technology Bombay India

ISBN: (纸本)9781450322010

An intcrprocedural analysis is precise if it is flow sensitive and fully context-sensitive even in the presence of recursion. Many methods of interprocedural analysis sacrifice precision for scalability while some are precise but limited to only a certain class of problems. Soot currently supports interprocedural analysis of Java programs using graph reachability. However, this approach is restricted to IFDS/IDE problems, and is not suitable for general data flow frameworks such as heap reference analysis and points-to analysis which have non-distributive flow functions. We describe a general-purpose interprocedural analysis framework for Soot using data flow values for context-sensitivity. This framework is not restricted to problems with distributive flow functions. although the lattice must be finite. It combines the key ideas of the tabulation method of the functional approach and the technique of value-based termination of call string construction. The efficiency and precision of interprocedural analyses is heavily affected by the precision of the underlying call graph. This is especially important for object-oriented languages like Java where virtual method invocations cause an explosion of spurious call edges if the call graph is constructed naively. We haw instantiated our framework with a flow and context-sensitive points-to analysis in Soot, which enables the construction of call graphs that are far more precise than those constructed by Soot's SPARK engine. Copyright © 2013 ACM.

关键词： data flow analysis