Top 10 Arxiv Papers Today in Programming Languages


0.0 Mikeys
#1. Bridging the Gap Between Programming Languages and Hardware Weak Memory Models
Anton Podkopaev, Ori Lahav, Viktor Vafeiadis
We develop a new intermediate weak memory model, IMM, as a way of modularizing the proofs of correctness of compilation from concurrent programming languages with weak memory consistency semantics to mainstream multi-core architectures, such as POWER and ARM. We use IMM to prove the correctness of compilation from the promising semantics of Kang et al. to POWER (thereby correcting and improving their result) and ARMv7, as well as to the recently revised ARMv8 model. Our results are mechanized in Coq, and to the best of our knowledge, these are the first machine-verified compilation correctness results for models that are weaker than x86-TSO.
more | pdf | html
Figures
None.
Tweets
HNTweets: Bridging the Gap Between Programming Languages and Hardware Weak Memory Models: https://t.co/WxHY2ep8js Comments: https://t.co/WnsxZ9aMQJ
hnbot: Bridging the Gap Between Programming Languages and Hardware Weak Memory Models (Discussion on HN - https://t.co/n63Jm5Y0Th) https://t.co/xZ8EnqBTLB
hn_frontpage: Bridging the Gap Between Programming Languages and Hardware Weak Memory Models L: https://t.co/QenpInM1Ru C: https://t.co/1DH78bMvoc
FrontPageHN: Bridging the Gap Between Programming Languages and Hardware Weak Memory Models https://t.co/Q0KH0v3HJp (cmts https://t.co/VF29uDE0ZR)
newsycombinator: Bridging the Gap Between Programming Languages and Hardware Weak Memory Models https://t.co/rgUwIr9sWM
bootstrap_tokyo: プログラミング言語とハードウェアの脆弱なメモリモデルのギャップを埋める https://t.co/G6n49yjzMd
angsuman: Bridging the Gap Between #Programming Languages and Hardware Weak Memory Models https://t.co/uZdSaOr1rF
hn_responder: Bridging the Gap Between Programming Languages and Hardware Weak Memory Models https://t.co/bRDUzkEjCI https://t.co/JC1piA4sP4
inf_anlun: Our paper "Bridging the Gap Between Programming Languages and Hardware Weak Memory Models" https://t.co/Jjbe1Iv6Do got accepted to #POPL19!
ZenrudMB: Bridging the Gap Between Programming Languages and Hardware Weak Memory Models https://t.co/kQpUwuhcTB #Bridging #Gap #ProgrammingLanguages
_mangesh_tekale: Bridging the Gap Between Programming Languages and Hardware Weak Memory Models https://t.co/iym32mcvPE
TridzOnline: Bridging the Gap Between Programming Languages and Hardware Weak Memory Models https://t.co/J9KTLvffJS
keep_posts: RT newsycombinator "Bridging the Gap Between Programming Languages and Hardware Weak Memory Models https://t.co/KFGgN9M9vC"
Github
None.
Youtube
None.
Other stats
Sample Sizes : None.
Authors: 3
Total Words: 19905
Unqiue Words: 3815

0.0 Mikeys
#2. Data Race Detection on Compressed Traces
Dileep Kini, Umang Mathur, Mahesh Viswanathan
We consider the problem of detecting data races in program traces that have been compressed using straight line programs (SLP), which are special context-free grammars that generate exactly one string, namely the trace that they represent. We consider two classical approaches to race detection --- using the happens-before relation and the lockset discipline. We present algorithms for both these methods that run in time that is linear in the size of the compressed, SLP representation. Typical program executions almost always exhibit patterns that lead to significant compression. Thus, our algorithms are expected to result in large speedups when compared with analyzing the uncompressed trace. Our experimental evaluation of these new algorithms on standard benchmarks confirms this observation.
more | pdf | html
Figures
None.
Tweets
ComputerPapers: Data Race Detection on Compressed Traces. https://t.co/cO8rJJirzH
Github
None.
Youtube
None.
Other stats
Sample Sizes : None.
Authors: 3
Total Words: 20184
Unqiue Words: 3623

0.0 Mikeys
#3. Multivariant Assertion-based Guidance in Abstract Interpretation
Isabel Garcia-Contreras, Jose F. Morales, Manuel V. Hermenegildo
Approximations during program analysis are a necessary evil, as they ensure essential properties, such as analysis soundness and termination, but they also imply that the analysis is not guaranteed to always produce useful results. In such cases it is necessary to have some means for users to provide information to guide analysis and thus to improve precision and/or shorten analysis time. This allows dealing with, e.g., constructs for which the analysis is not complete and loses precision or for which the source is only partially available. We present techniques for supporting within an abstract interpretation framework a rich set of assertions that can deal with multivariance/context-sensitivity, and can handle different run-time semantics for those assertions that cannot be discharged at compile time. We show how the proposed approach can be applied to both improving precision and accelerating convergence, and provide a procedure to decide whether the invariants used to guide the analyzer are checked, incompatible, or neither....
more | pdf | html
Figures
None.
Tweets
arxiv_cslo: Multivariant Assertion-based Guidance in Abstract Interpretation https://t.co/64ojXu82wf
arxiv_cslo: Multivariant Assertion-based Guidance in Abstract Interpretation https://t.co/64ojXu82wf
Github
None.
Youtube
None.
Other stats
Sample Sizes : None.
Authors: 3
Total Words: 8447
Unqiue Words: 2449

0.0 Mikeys
#4. Racets: Faceted Execution in Racket
Kristopher Micinski, Zhanpeng Wang, Thomas Gilray
Faceted Execution is a linguistic paradigm for dynamic information-flow control. Under faceted execution, secure program data is represented by faceted values: decision trees that encode how the data should appear to its owner (represented by a label) versus everyone else. When labels are allowed to be first-class (i.e., predicates that decide at runtime which data to reveal), faceted execution enables policy-agnostic programming: a programming style that allows privacy policies for data to be enforced independently of code that computes on that data. To date, implementations of faceted execution are relatively heavyweight: requiring either changing the language runtime or the application code (e.g., by using monads). Following Racket's languages-as-libraries approach, we present Racets: an implementation of faceted execution as a library of macros. Given Racket's highly-expressive macro system, our implementation follows relatively directly from the semantics of faceted execution. To demonstrate how Racets can be used for...
more | pdf | html
Figures
Tweets
krismicinski: @clegoues @chrisamaphone I feel like the bar should be "actually contributed to a workshop-level result in a thoughtful and direct way" rather than "eh, ran some data and pushed some buttons and edited some text for a top conf paper" (paper here https://t.co/OxAmEbfxl8 he wrote the code!)
krismicinski: Super happy to say that our @schemeworkshop paper on faceted execution as a racket language was accepted! Will be presented at Scheme '18 (colocated w/ @icfp_conference / @strangeloop_stl) in late September. paper here: https://t.co/OxAmEbfxl8
krismicinski: New Arxiv draft! Racets: Faceted Execution in Racket. First paper w/ my student Zhanpeng at @haverfordedu https://t.co/OxAmEbfxl8
ComputerPapers: Racets: Faceted Execution in Racket. https://t.co/K9NYvwxV4Q
taraw: RT @arxiv_org: Racets: Faceted Execution in Racket. https://t.co/ktPDWhp5X1 https://t.co/nCler0VsfE
esigma6: RT @arxiv_org: Racets: Faceted Execution in Racket. https://t.co/ktPDWhp5X1 https://t.co/nCler0VsfE
Github

Faceted execution in Racket

Repository: racets
User: fordsec
Language: TeX
Stargazers: 2
Subscribers: 4
Forks: 0
Open Issues: 0
Youtube
None.
Other stats
Sample Sizes : None.
Authors: 3
Total Words: 8399
Unqiue Words: 2379

0.0 Mikeys
#5. What Happens - After the First Race? Enhancing the Predictive Power of Happens - Before Based Dynamic Race Detection
Umang Mathur, Dileep Kini, Mahesh Viswanathan
Dynamic race detection is the problem of determining if an observed program execution reveals the presence of a data race in a program. The classical approach to solving this problem is to detect if there is a pair of conflicting memory accesses that are unordered by Lamport's happens-before (HB) relation. HB based race detection is known to not report false positives, i.e., it is sound. However, the soundness guarantee of HB only promises that the first pair of unordered, conflicting events is a schedulable data race. That is, there can be pairs of HB-unordered conflicting data accesses that are not schedulable races because there is no reordering of the events of the execution, where the events in race can be executed immediately after each other. We introduce a new partial order, called schedulable happens-before (SHB) that exactly characterizes the pairs of schedulable data races --- every pair of conflicting data accesses that are identified by SHB can be scheduled, and every HB-race that can be scheduled is identified by...
more | pdf | html
Figures
None.
Tweets
ComputerPapers: What Happens - After the First Race? Enhancing the Predictive Power of Happens - Before Based Dynamic Race Detection. https://t.co/ktmZm21dNs
Github
None.
Youtube
None.
Other stats
Sample Sizes : None.
Authors: 3
Total Words: 21760
Unqiue Words: 3689

0.0 Mikeys
#6. AppIntent: Intuitive Automation Specification Framework for Mobile AppTesting
Poornima Gopi
The proliferation of mobile apps and reduced time in mobile app releases mandates the need for faster and efficient testing of mobile apps, their GUI and functional capabilities. Though, there are wide variety of open source tools and frameworks that are developed to provide automated test infrastructure for testing mobile apps. Each of these automation tools supports different scripting languages for automating the app testing. These frameworks fundamentally lacks the ability to directly capture the intent of the users who intend to effectively test the mobile app and its cross-app functional capabilities and performance without worrying about the low-level scripting language associated with each tool. Hence, to address this limitation, we propose a high-level intent-based automation specification language and APIs that could effectively address following aspects: (i)capture the test automation steps to be captured as high-level intents using intuitive automation specification language, and (ii) provides framework support...
more | pdf | html
Figures
Tweets
arxiv_org: AppIntent: Intuitive Automation Specification Framework for Mobile AppTesting. https://t.co/udAb0fUp32 https://t.co/4wr7yEcL5X
ComputerPapers: AppIntent: Intuitive Automation Specification Framework for Mobile AppTesting. https://t.co/fB5FB32O2V
Rosenchild: RT @arxiv_org: AppIntent: Intuitive Automation Specification Framework for Mobile AppTesting. https://t.co/udAb0fUp32 https://t.co/4wr7yEcL…
HubBucket: RT @arxiv_org: AppIntent: Intuitive Automation Specification Framework for Mobile AppTesting. https://t.co/udAb0fUp32 https://t.co/4wr7yEcL…
Github
None.
Youtube
None.
Other stats
Sample Sizes : None.
Authors: 1
Total Words: 3372
Unqiue Words: 1123

0.0 Mikeys
#7. Reference Type Logic Variables in Constraint-logic Object-oriented Programming
Jan C. Dageförde
Constraint-logic object-oriented programming, for example using Muli, facilitates the integrated development of business software that occasionally involves finding solutions to constraint-logic problems. So far, Muli covers the application of constraints to (logic) variables that are of primitive types. Our work generalises this in order to facilitate (constraint) logic programming involving free objects, i. e. for reference type variables. This includes invocations on free objects and constraints over object types, while taking arbitrary class hierarchies of a Java-based language into account. This work discusses interactions between a constraint-logic object-oriented language and reference type logic variables, particularly invocations on and access to logic variables, typecasts, and equality, and proposes approaches as to how these interactions can be handled.
more | pdf | html
Figures
None.
Tweets
M157q_News_RSS: Reference Type Logic Variables in Constraint-logic Object-oriented Programming. (arXiv:1808.08185v1 [https://t.co/okMwBtlQAe]) https://t.co/zLlANNVBdR Constra
ComputerPapers: Reference Type Logic Variables in Constraint-logic Object-oriented Programming. https://t.co/O7ho1Xa5MA
Github
None.
Youtube
None.
Other stats
Sample Sizes : None.
Authors: 1
Total Words: 5349
Unqiue Words: 1558

0.0 Mikeys
#8. Enhancing POI testing approach through the use of additional information
Sergio Pérez, Salvador Tamarit
Recently, a new approach to perform regression testing has been defined: the point of interest (POI) testing. A POI, in this context, is any expression of a program. The approach receives as input a set of relations between POIs from a version of a program and POIs from another version, and also a sequence of input functions, i.e. test cases. Then, a program instrumentation, an input test case generation and different comparison functions are used to obtain the final report which indicates whether the alternative version of the program behaves as expected, e.g. it produces the same values or it uses less CPU/memory. In this paper, we explain how we can improve the POI testing approach through the use of common stack traces and a more sophisticated tracing for calls. These enhancements of the approach allow users to identify errors earlier and easier. Additionally, they enable new comparison modes and new categories of reported unexpected behaviours.
more | pdf | html
Figures
None.
Tweets
M157q_News_RSS: Enhancing POI testing approach through the use of additional information. (arXiv:1808.07938v1 [https://t.co/okMwBtlQAe]) https://t.co/hh7lJ6pcjG Recently, a n
Github

SecEr: Erlang Code Evolution Control Tool

Repository: secer
User: mistupv
Language: Erlang
Stargazers: 0
Subscribers: 2
Forks: 0
Open Issues: 0
Youtube
None.
Other stats
Sample Sizes : None.
Authors: 2
Total Words: 12235
Unqiue Words: 2750

0.0 Mikeys
#9. Runtime verification in Erlang by using contracts
Lars-Åke Fredlund, Julio Mariño, Sergio Pérez, Salvador Tamarit
During its lifetime, a program suffers several changes that seek to improve or to augment some parts of its functionality. However, these modifications usually also introduce errors that affect the already-working code. There are several approaches and tools that help to spot and find the source of these errors. However, most of these errors could be avoided beforehand by using some of the knowledge that the programmers had when they were writing the code. This is the idea behind the design-by-contract approach, where users can define contracts that can be checked during runtime. In this paper, we apply the principles of this approach to Erlang, enabling, in this way, a runtime verification system in this language. We define two types of contracts. One of them can be used in any Erlang program, while the second type is intended to be used only in concurrent programs. We provide the details of the implementation of both types of contracts. Moreover, we provide an extensive explanation of each contract as well as examples of their...
more | pdf | html
Figures
Tweets
M157q_News_RSS: Runtime verification in Erlang by using contracts. (arXiv:1808.07937v1 [https://t.co/okMwBtlQAe]) https://t.co/BVBlqKdvxT During its lifetime, a program suffe
ComputerPapers: Runtime verification in Erlang by using contracts. https://t.co/GMK6ybYFGr
Github

Erlang Design by Contract

Repository: edbc
User: tamarit
Language: Erlang
Stargazers: 2
Subscribers: 1
Forks: 0
Open Issues: 0
Youtube
None.
Other stats
Sample Sizes : None.
Authors: 4
Total Words: 8971
Unqiue Words: 2293

0.0 Mikeys
#10. Competitive Parallelism: Getting Your Priorities Right
Stefan K. Muller, Umut A. Acar, Robert Harper
Multi-threaded programs have traditionally fallen into one of two domains: cooperative and competitive. These two domains have traditionally remained mostly disjoint, with cooperative threading used for increasing throughput in compute-intensive applications such as scientific workloads and cooperative threading used for increasing responsiveness in interactive applications such as GUIs and games. As multicore hardware becomes increasingly mainstream, there is a need for bridging these two disjoint worlds, because many applications mix interaction and computation and would benefit from both cooperative and competitive threading. In this paper, we present techniques for programming and reasoning about parallel interactive applications that can use both cooperative and competitive threading. Our techniques enable the programmer to write rich parallel interactive programs by creating and synchronizing with threads as needed, and by assigning threads user-defined and partially ordered priorities. To ensure important responsiveness...
more | pdf | html
Figures
None.
Tweets
Github
None.
Youtube
None.
Other stats
Sample Sizes : None.
Authors: 3
Total Words: 24552
Unqiue Words: 4232

About

Assert is a website where the best academic papers on arXiv (computer science, math, physics), bioRxiv (biology), BITSS (reproducibility), EarthArXiv (earth science), engrXiv (engineering), LawArXiv (law), PsyArXiv (psychology), SocArXiv (social science), and SportRxiv (sport research) bubble to the top each day.

Papers are scored (in real-time) based on how verifiable they are (as determined by their Github repos) and how interesting they are (based on Twitter).

To see top papers, follow us on twitter @assertpub_ (arXiv), @assert_pub (bioRxiv), and @assertpub_dev (everything else).

To see beautiful figures extracted from papers, follow us on Instagram.

Tracking 72,995 papers.

Search
Sort results based on if they are interesting or reproducible.
Interesting
Reproducible
Categories
All
Astrophysics
Cosmology and Nongalactic Astrophysics
Earth and Planetary Astrophysics
Astrophysics of Galaxies
High Energy Astrophysical Phenomena
Instrumentation and Methods for Astrophysics
Solar and Stellar Astrophysics
Condensed Matter
Disordered Systems and Neural Networks
Mesoscale and Nanoscale Physics
Materials Science
Other Condensed Matter
Quantum Gases
Soft Condensed Matter
Statistical Mechanics
Strongly Correlated Electrons
Superconductivity
Computer Science
Artificial Intelligence
Hardware Architecture
Computational Complexity
Computational Engineering, Finance, and Science
Computational Geometry
Computation and Language
Cryptography and Security
Computer Vision and Pattern Recognition
Computers and Society
Databases
Distributed, Parallel, and Cluster Computing
Digital Libraries
Discrete Mathematics
Data Structures and Algorithms
Emerging Technologies
Formal Languages and Automata Theory
General Literature
Graphics
Computer Science and Game Theory
Human-Computer Interaction
Information Retrieval
Information Theory
Machine Learning
Logic in Computer Science
Multiagent Systems
Multimedia
Mathematical Software
Numerical Analysis
Neural and Evolutionary Computing
Networking and Internet Architecture
Other Computer Science
Operating Systems
Performance
Programming Languages
Robotics
Symbolic Computation
Sound
Software Engineering
Social and Information Networks
Systems and Control
Economics
Econometrics
General Economics
Theoretical Economics
Electrical Engineering and Systems Science
Audio and Speech Processing
Image and Video Processing
Signal Processing
General Relativity and Quantum Cosmology
General Relativity and Quantum Cosmology
High Energy Physics - Experiment
High Energy Physics - Experiment
High Energy Physics - Lattice
High Energy Physics - Lattice
High Energy Physics - Phenomenology
High Energy Physics - Phenomenology
High Energy Physics - Theory
High Energy Physics - Theory
Mathematics
Commutative Algebra
Algebraic Geometry
Analysis of PDEs
Algebraic Topology
Classical Analysis and ODEs
Combinatorics
Category Theory
Complex Variables
Differential Geometry
Dynamical Systems
Functional Analysis
General Mathematics
General Topology
Group Theory
Geometric Topology
History and Overview
Information Theory
K-Theory and Homology
Logic
Metric Geometry
Mathematical Physics
Numerical Analysis
Number Theory
Operator Algebras
Optimization and Control
Probability
Quantum Algebra
Rings and Algebras
Representation Theory
Symplectic Geometry
Spectral Theory
Statistics Theory
Mathematical Physics
Mathematical Physics
Nonlinear Sciences
Adaptation and Self-Organizing Systems
Chaotic Dynamics
Cellular Automata and Lattice Gases
Pattern Formation and Solitons
Exactly Solvable and Integrable Systems
Nuclear Experiment
Nuclear Experiment
Nuclear Theory
Nuclear Theory
Physics
Accelerator Physics
Atmospheric and Oceanic Physics
Applied Physics
Atomic and Molecular Clusters
Atomic Physics
Biological Physics
Chemical Physics
Classical Physics
Computational Physics
Data Analysis, Statistics and Probability
Physics Education
Fluid Dynamics
General Physics
Geophysics
History and Philosophy of Physics
Instrumentation and Detectors
Medical Physics
Optics
Plasma Physics
Popular Physics
Physics and Society
Space Physics
Quantitative Biology
Biomolecules
Cell Behavior
Genomics
Molecular Networks
Neurons and Cognition
Other Quantitative Biology
Populations and Evolution
Quantitative Methods
Subcellular Processes
Tissues and Organs
Quantitative Finance
Computational Finance
Economics
General Finance
Mathematical Finance
Portfolio Management
Pricing of Securities
Risk Management
Statistical Finance
Trading and Market Microstructure
Quantum Physics
Quantum Physics
Statistics
Applications
Computation
Methodology
Machine Learning
Other Statistics
Statistics Theory
Feedback
Online
Stats
Tracking 72,995 papers.