Combinations pals lcr problem12 label0

[lembergerth]

[ This PR is a part of #1104 and depends on #1212 and #1214 ]

Description of tasks

New benchmark tasks that are a combination of existing benchmark tasks
from seq-mthreaded/pals_lcr* and eca-rers2012/Problem12_label0*.

Each benchmark task in this directory is created from two other tasks, according to the following pattern:

/* definitions of Task 1 ... */
int main1() { /* main-method of Task 1 ... */ }
/* definitions of Task 2 ... */
int main2() { /* main-method of Task 2 ... */ }

int main() {
  if (__VERIFIER_nondet_int()) {
    main1();
  } else {
    main2();
  }

Definitions are renamed to avoid conflicts, if necessary.

This construction leads to programs with independent program parts.

Open Issue: Licensing

I'm not sure about how to license these tasks.
Some of the tasks that we used are part of sv-benchmarks, but do not have a separate license in their corresponding directory.
For now, I have written a LICENSE.txt that coarsely references the original licenses (if present),
but I don't think this is good enough.

I'd be happy about any constructive input on this matter.

Checklist

• programs added to new and appropriately named directory

• license present and acceptable (either in separate file or as comment at beginning of program)

• contributed-by present (either in README file or as comment at beginning of program)

• programs added to a .set file of an existing category, or new sub-category established (if justified)

• intended property matches the corresponding .prp file

• programs and expected answer added to a .yml file according to task definitions

• architecture (32 bit vs. 64 bit) matches the corresponding .cfg file
• original sources present
• preprocessed files present
• preprocessed files generated with correct architecture
• Makefile added with correct content and without overly broad suppression of warnings

[lembergerth]

@PhilippWendler regarding the licensing issue:

Content contributors to eca-rers2012 were Philipp Wendler and Dirk Beyer (cd13b12).
There's no copyright in the corresponding license, so I assume the copyright is by the SV-benchmarks community.

seq_mthreaded tasks are copyrighted and licensed by CMU, but as you already mentioned, it is not clear from which systems these tasks were created from.
I did some internet search but couldn't find any information. Is it good enough to trust the contributors that the license is valid?

In addition, seq_mthreaded tasks are under a special license. Is this the correct way to reference that license in the SPDX header?

// SPDX-License-Identifier: SEE LICENSE IN LICENSE_pals.txt

(SPDX identifier to eca-rers2012 are still being processed, will be commited once done)

[PhilippWendler]

Can you please file separate PRs for changes to existing tasks and new tasks? Because ECA and seq-mthreaded have nothing in common in regard to license and copyright and relevant discussions would be different, I would prefer separate PRs for these even. (The rest of this comment already shows that we have 3 separate discussion topics for 2 licensing questions and the new tasks here and this would be better in 3 PRs.)

Content contributors to eca-rers2012 were Philipp Wendler and Dirk Beyer (cd13b12).
There's no copyright in the corresponding license, so I assume the copyright is by the SV-benchmarks community.

These benchmarks were taken from external sources (RERS), so there exists at least one additional copyright holder. We are not required to list it, but I guess it would be good to represent the state of the copyright better. (Some people also mistakenly assume that the listed copyright holders are the authors of the files.) In this case it should not be difficult, it is either Bernhard Steffen or something like "The RERS Competition". @dbeyer Do you know more?

seq_mthreaded tasks are copyrighted and licensed by CMU, but as you already mentioned, it is not clear from which systems these tasks were created from.
I did some internet search but couldn't find any information. Is it good enough to trust the contributors that the license is valid?

I would say this depends on how plausible it is that these programs were created from CMU sources alone. For example, if obviously identifiable references to other programs occur as sources in readmes, file names, program identifiers, or respective papers, then we should investigate more. If nothing of this exists, then I guess we can live with the risk.

(Legally it is clear that "we trusted somebody else to properly declare the license and handled accordingly" does not help at all, we are fully responsible for what we redistribute and need to fulfill the license requirements that are attached to each part of the sources.)

It is probably also a good idea to list the SV-Benchmarks community as additional copyright holder, also for making it clear that the files were changed.

In addition, seq_mthreaded tasks are under a special license. Is this the correct way to reference that license in the SPDX header?

// SPDX-License-Identifier: SEE LICENSE IN LICENSE_pals.txt

No, the correct form uses LicenseRef. It is also a good custom to name custom licenses in a way that refers to the well-known license on which they are based, if one exists. For example, SPDX has MIT and MIT-CMU. In BenchExec, I used LicenseRef-BSD-3-Clause-CMU for a similar license as the one that is used here. This already gives an idea to users what the license contains.

For the seq_mthreaded license, it is quite similar to BSD-3-Clause-Attribution, but with an additional clause inserted. However, because the inserted clause in practice adds little compared to what clause 3 already requires, I would say that LicenseRef-BSD-3-Clause-Attribution-CMU is a quite accurate name that indicates reasonably well to readers what they should expect.

[lembergerth]

Can you please file separate PRs for changes to existing tasks and new tasks?

Done for seq-mthreaded. reuse is still not done with adding headers to the ECA tasks, but I will create a PR for their metadata changes once it is.

[lembergerth]

I've updated the combined tasks with the updated licensing information present in seq-mthreaded and eca-rers2012.

Sorry for the force-push mess.