Skip to content

Concurrency: treat updates to an unknown field as atomic #6123

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
May 12, 2023
Merged

Concurrency: treat updates to an unknown field as atomic #6123

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
19 changes: 19 additions & 0 deletions regression/cbmc-concurrency/array1/main.c
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,19 @@
int data[2];
unsigned sync;

void thread()
{
data[sync % 2] = 1;
__CPROVER_assert(data[sync % 2] == 1, "1");
}

int main()
{
unsigned nondet;
sync = nondet;
__CPROVER_ASYNC_1:
thread();
unsigned sync_value = sync;
data[(sync_value + 1) % 2] = 2;
__CPROVER_assert(data[(sync_value + 1) % 2] == 2, "2");
}
8 changes: 8 additions & 0 deletions regression/cbmc-concurrency/array1/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
CORE
main.c

^EXIT=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL$
--
^warning: ignoring
18 changes: 18 additions & 0 deletions src/goto-symex/goto_symex.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -117,10 +117,28 @@ void goto_symext::symex_assign(
return;
}

// We may end up reading (and writing) all components of an object composed
// of multiple fields. In such cases, we must do so atomically to avoid
// overwriting components modified by another thread. Note that this also
// implies multiple shared reads on the rhs being treated as atomic.
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks for the comment that makes this clear but ... I am a little concerned about this because now
struct s = t; and

struct s;
s.x = t.x;
s.y = t.y;

can have different behaviour. I guess there is a very valid question about what the atomic actions in the CPROVER concurrency model are.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Although this case shouldn't arise for structs and mainly affects arrays: you are absolutely right that this is questionable either way. Without this patch, we'll have spurious results (as documented in the regression test). With this patch, we may miss some behaviour, depending on what exactly we otherwise consider to be atomic.

const bool maybe_divisible =
lhs.id() == ID_index ||
(is_ssa_expr(lhs) &&
state.field_sensitivity.is_divisible(to_ssa_expr(lhs), false));
const bool need_atomic_section = maybe_divisible &&
state.threads.size() > 1 &&
state.atomic_section_id == 0;

if(need_atomic_section)
symex_atomic_begin(state);

exprt::operandst lhs_if_then_else_conditions;
symex_assignt{
shadow_memory, state, assignment_type, ns, symex_config, target}
.assign_rec(lhs, expr_skeletont{}, rhs, lhs_if_then_else_conditions);

if(need_atomic_section)
symex_atomic_end(state);
}
}

Expand Down