Skip to content
GitLab
Explore
Sign in
Primary navigation
Search or go to…
Project
P
publications
Manage
Activity
Members
Labels
Plan
Issues
Issue boards
Milestones
Code
Merge requests
Repository
Branches
Commits
Tags
Repository graph
Compare revisions
Build
Pipelines
Jobs
Pipeline schedules
Artifacts
Deploy
Releases
Container Registry
Model registry
Operate
Environments
Monitor
Incidents
Service Desk
Analyze
Value stream analytics
Contributor analytics
CI/CD analytics
Repository analytics
Model experiments
Help
Help
Support
GitLab documentation
Compare GitLab plans
Community forum
Contribute to GitLab
Provide feedback
Keyboard shortcuts
?
Snippets
Groups
Projects
Show more breadcrumbs
Verified Software
publications
Commits
7109ef60
Commit
7109ef60
authored
4 years ago
by
pmaksimo
Browse files
Options
Downloads
Patches
Plain Diff
minor corrections
parent
35e54b0b
No related branches found
Branches containing commit
No related tags found
No related merge requests found
Changes
1
Hide whitespace changes
Inline
Side-by-side
Showing
1 changed file
publications.bib
+47
-47
47 additions, 47 deletions
publications.bib
with
47 additions
and
47 deletions
publications.bib
+
47
−
47
View file @
7109ef60
...
...
@@ -1756,26 +1756,26 @@ school = {Imperial College London},
year
=
{2020}
,
type
=
{phdthesis}
,
project
=
{concurrency}
,
abstract
=
{The cloud has become popular for its low cost, high availability and
high fault-tolerance-queue or de-queue, for example Amazon Web Service (AWS) and
Google Cloud Platform (GCP. Those cloud infrastructures provide fixed interface,
to hide the complex internal implementation that consists of hundreds of thousands
of machines globally that work together as a whole system, known as a distributed
system. Clients of those systems only need to work with the abstract interfaces.
Transactions are the de facto interfaces in modern distributed databases.
Because of the CAP theorem, a distributed system must sacrifice strong consistency
to achieve high availability and high fault-tolerance. Engineers and researchers
have proposed many reference implementations in specific setting for various weak
consistency models. However, there have been little work on formalising the interfaces.
We introduce an interleaving operational semantics for describing such interfaces,
with the focus on the client-observable behaviour of atomic transactions on
distributed key-value stores. Our semantics builds on abstract states comprising
centralised, global key-value stores and partial client views. We provide
operational definitions of consistency models for our key-value stores which
are shown to be equivalent to the well-known declarative definitions of consistency
models for execution graphs. We explore two immediate applications of our semantics:
specific protocols of databases for a specific consistency can be verified in
our centralised semantics; programs can be directly shown to have invariant
abstract
=
{The cloud has become popular for its low cost, high availability and
high fault-tolerance-queue or de-queue, for example Amazon Web Service (AWS) and
Google Cloud Platform (GCP. Those cloud infrastructures provide fixed interface,
to hide the complex internal implementation that consists of hundreds of thousands
of machines globally that work together as a whole system, known as a distributed
system. Clients of those systems only need to work with the abstract interfaces.
Transactions are the de facto interfaces in modern distributed databases.
Because of the CAP theorem, a distributed system must sacrifice strong consistency
to achieve high availability and high fault-tolerance. Engineers and researchers
have proposed many reference implementations in specific setting for various weak
consistency models. However, there have been little work on formalising the interfaces.
We introduce an interleaving operational semantics for describing such interfaces,
with the focus on the client-observable behaviour of atomic transactions on
distributed key-value stores. Our semantics builds on abstract states comprising
centralised, global key-value stores and partial client views. We provide
operational definitions of consistency models for our key-value stores which
are shown to be equivalent to the well-known declarative definitions of consistency
models for execution graphs. We explore two immediate applications of our semantics:
specific protocols of databases for a specific consistency can be verified in
our centralised semantics; programs can be directly shown to have invariant
properties such as robustness results against a weak consistency model.}
,
}
...
...
@@ -1788,40 +1788,40 @@ title = {Data Consistency in Transactional Storage Systems: a Centralised Ap
booktitle
=
{34th European Conference on Object-Oriented Programming (ECOOP 2020)}
,
project
=
{concurrency}
,
year
=
{2020}
,
abstract
=
{We introduce an interleaving operational semantics for describing the
client-observable behaviour of atomic transactions on distributed key-value stores.
Our semantics builds on abstract states comprising centralised, global key-value
stores and partial client views. We provide operational definitions of consistency
models for our abstract states which we show to be equivalent to the well known
declarative definitions of consistency model on abstract executions. We explore
two applications, verifying that the COPS replicated database and the Clock-SI
partitioned database satisfy their consistency models using trace refinement,
abstract
=
{We introduce an interleaving operational semantics for describing the
client-observable behaviour of atomic transactions on distributed key-value stores.
Our semantics builds on abstract states comprising centralised, global key-value
stores and partial client views. We provide operational definitions of consistency
models for our abstract states which we show to be equivalent to the well known
declarative definitions of consistency model on abstract executions. We explore
two applications, verifying that the COPS replicated database and the Clock-SI
partitioned database satisfy their consistency models using trace refinement,
and proving invariant properties of client programs.}
,
}
@InProceedings
{
Sampaio2020Trusted
,
author
=
{Gabriela Sampaio and
Jos{\'{e}} {Fragoso Santos} and
Petar Maksimovi\'{c}
and Philippa Gardner}
,
author
=
{Gabriela Sampaio and
Jos{\'{e}} {Fragoso Santos} and
Petar Maksimovi\'{c}
and Philippa Gardner}
,
title
=
{A Trusted Infrastructure for Symbolic Analysis of Event-Driven Web Applications}
,
booktitle
=
{34th European Conference on Object-Oriented Programming (ECOOP 2020)}
,
project
=
{
gillian
}
,
project
=
{
web
}
,
year
=
{2020}
,
abstract
=
{We introduce a trusted infrastructure for symbolic analysis of modern
event-driven Web applications. This infrastructure consists of reference
implementations of the DOM Core Level 1 and UI Events, JavaScript Promises,
and the JavaScript async/await APIs, all underpinned by a simple Core Event
Semantics that is sufficiently expressive to describe the event models underlying
all these APIs. Our reference implementations are trustworthy in that they follow
the API respective standards line-by-line and they are thoroughly tested against
the appropriate official test-suites, passing all the applicable tests. Using the
Core Events Semantics and the reference implementations, we develop JaVerT.Click,
a symbolic execution tool for JavaScript that, for the first time, supports reasoning
about JavaScript programs that use some (possibly all) these APIs. Using JaVerT.Click,
we perform comprehensive symbolic testing of the events module of Cash, a widely-used jQuery
alternative, creating a symbolic test suite with 100 per cent line coverage, establishing bounded
correctness of several essential properties of the module, and discovering two subtle,
abstract
=
{We introduce a trusted infrastructure for symbolic analysis of modern
event-driven Web applications. This infrastructure consists of reference
implementations of the DOM Core Level 1 and UI Events, JavaScript Promises,
and the JavaScript async/await APIs, all underpinned by a simple Core Event
Semantics that is sufficiently expressive to describe the event models underlying
all these APIs. Our reference implementations are trustworthy in that they follow
the API respective standards line-by-line and they are thoroughly tested against
the appropriate official test-suites, passing all the applicable tests. Using the
Core Events Semantics and the reference implementations, we develop JaVerT.Click,
a symbolic execution tool for JavaScript that, for the first time, supports reasoning
about JavaScript programs that use some (possibly all) these APIs. Using JaVerT.Click,
we perform comprehensive symbolic testing of the events module of Cash, a widely-used jQuery
alternative, creating a symbolic test suite with 100 per cent line coverage, establishing bounded
correctness of several essential properties of the module, and discovering two subtle,
previously unknown bugs.}
,
}
...
...
This diff is collapsed.
Click to expand it.
Preview
0%
Loading
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Save comment
Cancel
Please
register
or
sign in
to comment